on e105606 help sign in
13 files
../ Binary.hsContext for "Can't find implementation" CaseTree.hsAdd location for No pattern clauses error 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.hsprim__believeMe needs to be considered total 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