git.iko.soy/Idris-dev
on 2aaff41 help sign in
Idris-dev/src/Idris/Core
13 files
../ Binary.hsSend serialized versions of TT terms in pprint CaseTree.hsEnsure erasure happens under 'force' Constraints.hsStrictness annotations DeepSeq.hsAdd a special name for instance constructors. Elaborate.hsMore efficiency improvements Evaluate.hsBetter treatment of unbound implicits Execute.hsStop erasing binder types in executor ProofState.hsUse a zipper-like proof state ProofTerm.hsRecord import paths in ibc TC.hsFuture-proof the TC' monad TT.hsStop erasing binder types in executor Typecheck.hsConversion checking tweak Unify.hsUse a zipper-like proof state