on 0222012 help sign in
13 files
../ Binary.hsContext for "Can't find implementation" CaseTree.hsfindCalls should find constructors too Constraints.hsuniverse inconsistency errors can originate from two places. make the error message consistent between these two. DeepSeq.hsFix behaviour of %hide Elaborate.hsNormalise type when introducing lambda Evaluate.hsFix silly error in totality checker Execute.hsFile IO type indicates possibility of failure ProofState.hsAdd the ability to define datatypes in Elab ProofTerm.hsRemove dubious matching rule TT.hsUse exact name lookup for hiding Typecheck.hsSimplify reflection and Raw Unify.hsDisplay expected type of RHS in error messages WHNF.hsConvert comments in WHNF.hs to Haddock