ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity
3034fb619c
Idris-dev/test/meta002
History
David Raymond Christiansen f09605b3dd Require unique global names in TT 
Fixes #2217 by demanding that global names in TT terms be
unambiguous. The elaborator will always produce them that way, but user
elab scripts might not, which led to confusion.

Also, disentagle 'apply' and 'fill'.
2015-04-30 12:40:36 +02:00
..
expected Add reasonable tests for elaborator reflection 2015-04-23 23:18:44 +02:00
run Add reasonable tests for elaborator reflection 2015-04-23 23:18:44 +02:00
Tacs.idr Require unique global names in TT 2015-04-30 12:40:36 +02:00