git.iko.soy/Idris-dev
on master help sign in
history of0140e67..master
compare
0655d3dAllow syntax rules at the declaration levelEdwin Brady cd1d1c8Fix showing of negative numbers in primitive typesMelvar Chen 766b73aLook up operator fixity in ElabDavid Raymond Christiansen b693b81Merge pull request #2540 from david-christiansen/wip/tacticalDavid Christiansen 77324bdMerge pull request #2539 from david-christiansen/hl-kwDavid Christiansen ab63941Added top-level %runElab supportDavid Raymond Christiansen 239c8caMove resolveTC to ProofSearch.hsEdwin Brady 3288a6cFix coverage checker for sigma typesEdwin Brady fbb201cMerge branch 'hl-kw' into wip/tacticalDavid Raymond Christiansen d741a30Extra info for errors in advanced modeDavid Raymond Christiansen 1c87b5eThread the fresh name counter through runElabDavid Raymond Christiansen 6ada023Better error when asking for non-existent goal typeDavid Raymond Christiansen 90b7d07Point readers at Elaborator ReflectionJeremy W. Sherman 156fb5aDocument interactive theorem proving as deprecated.Jeremy W. Sherman