Idris2-boot

edwinb/Idris2-boot

Fork 0

mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-23 03:05:00 +03:00

Commit Graph

Author	SHA1	Message	Date
Edwin Brady	146c301f6c	Change main program to be Idris2 With the --yaffle flag, you get the old behaviour which is to invoke the checker for the core theory (and all the tests are updated appropriately for this).	2019-06-09 11:58:29 +01:00
Edwin Brady	a59a104230	Implement 'rewrite' expressions Mostly direct from Blodwen (some minor modifications to deal with new way of going into a new scope in the elaborator as well as the usual bits dealing with name lookup and Glued terms)	2019-05-27 12:15:37 +01:00

Author

SHA1

Message

Date

Edwin Brady

146c301f6c

Change main program to be Idris2

With the --yaffle flag, you get the old behaviour which is to invoke the
checker for the core theory (and all the tests are updated appropriately
for this).

2019-06-09 11:58:29 +01:00

Edwin Brady

a59a104230

Implement 'rewrite' expressions

Mostly direct from Blodwen (some minor modifications to deal with new
way of going into a new scope in the elaborator as well as the usual
bits dealing with name lookup and Glued terms)

2019-05-27 12:15:37 +01:00

2 Commits