Idris2/src
Edwin Brady ebc413ede5 Postpone elaborating lambdas
It's worth delaying in case doing some more work (and some more
interface resolution) can make the type more concrete. This makes
test linear011 work more smoothly, and will help with this sort of
program in general.

A better way, later, would be to try elaborating and delay only if the
type is not yet known. We have the facilities, but it's too fiddly for
me to want to implement it right now...
2020-06-24 23:27:45 +01:00
..
Algebra Add visibility rules on types 2020-05-30 17:03:15 +01:00
Compiler Silence compile message when compiling Chez programs 2020-06-20 17:23:51 +02:00
Core Determining argument check below top level 2020-06-24 22:07:52 +01:00
Data Add missing totality annotations 2020-05-28 15:17:14 +01:00
Idris change namespace parser to have minimum indentation 2020-06-21 20:17:00 +01:00
Parser Merge pull request #315 from ShinKage/repl-import-module 2020-06-20 20:51:17 +02:00
Text Remove todo 2020-06-13 23:52:54 +02:00
TTImp Postpone elaborating lambdas 2020-06-24 23:27:45 +01:00
Utils Replace FFI implementation of 'hex' function with a plain Idris version 2020-06-16 01:40:28 +02:00
Yaffle Make pathToNS handle absolute path 2020-05-30 21:43:48 +08:00
Algebra.idr Add missing totality annotations 2020-05-28 15:17:14 +01:00