edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-25 05:43:19 +03:00
Code Issues Projects Releases Wiki Activity
A dependently typed programming language, a successor to Idris
12 Commits 2 Branches 1 Tag 4.2 MiB
Idris 97.3%
C 1.3%
Scheme 0.6%
Makefile 0.4%
Racket 0.3%
7d672407c8
Go to file
Edwin Brady 7d672407c8 Start on UnifyState 
Also removed 'MV' as a special name type, and added a Meta constructor
in TT which is applied to exactly the right number of arguments for the
environment the meta was constructed in.

It's possible the local unification UCtxt may be more trouble than it's
worth! Instead perhaps we can try let binding unification solutions where
possible on leaving the scope in which they're introduced.
2019-03-17 20:43:51 +00:00
sample Add Weaken interface, to start evaluator 2019-03-10 22:00:10 +00:00
src Start on UnifyState 2019-03-17 20:43:51 +00:00
yaffle.ipkg Start on UnifyState 2019-03-17 20:43:51 +00:00