on 54e4e41 help sign in
all commits
3cd25e6Add extra HL information to PRefDavid Raymond Christiansen 727a3d6Fix transform elaborationEdwin Brady c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen 673a1fcTweak for types of case blocksEdwin Brady b5dd402Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 289c05fHeuristic for generating better metavar typesEdwin Brady d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 04b4cc0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen e32e899Totality checking for functions defined in Elab scriptsDavid Raymond Christiansen c380421Move ElabTerm into Elab.TermEdwin Brady f4aaf01Guard !! in forgetEnvEdwin Brady c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen 426d052Add provenance flag to unification errorsEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady 2c39286Fix for name clashes when applying transformationsEdwin Brady 3ade599Partial evaluator fixesEdwin Brady 37748ceAdd transformation rules for partial evaluationEdwin Brady