on cf47310 help sign in
13 files
../ Binary.hsAdded top-level %runElab support CaseTree.hsPropagate errors originating from case trees Constraints.hsRicher universe error objects DeepSeq.hsAdded top-level %runElab support Elaborate.hsMerge pull request #2540 from david-christiansen/wip/tactical Evaluate.hsFinish WHNF for operators Execute.hsProof search should only use user visible names ProofState.hsUse subst for intro, rather than updsubst ProofTerm.hsMark 'complete' terms to save time in elaboration TT.hsAdded top-level %runElab support Typecheck.hsProof search should only use user visible names Unify.hsImprove disambiguation a bit more WHNF.hsFinish WHNF for operators