../ CaseTree.hsMake Haddock able to parse Idris's source14 years ago Constraints.hsFix non-termination error in universe checker14 years ago CoreParser.hsAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!14 years ago Elaborate.hsMake Haddock able to parse Idris's source14 years ago Evaluate.hsMerge branch 'master' into bitstring14 years ago ProofShell.hsDisentangle Haskeline from the internals Idris14 years ago ProofState.hsChanged approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.14 years ago ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!14 years ago Typecheck.hsMerge branch 'bitstring' of https://github.com/bitlisp/Idris-dev into bitlisp-bitstring14 years ago Unify.hsHNF in unification to speed things up14 years ago