search

mwleeds / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Demo: not having a deBruijn in the programming problem #87

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
When working on a programming problem, we have:

 > let plus (m : Nat)(n : Nat) : Nat
Let there be plus.
\ m : Nat ->
\ n : Nat ->
Programming: < plus^1 m n : Nat >

This "plus^1" is a nuisance.

Original issue reported on code.google.com by pedag...@gmail.com on 7 Sep 2010 at 10:40

GoogleCodeExporter commented 9 years ago 
A cheap solution would be to make the distiller ignore de Bruijn indices for 
FAKE references (since they aren't in scope anyway).

Original comment by adamgundry on 7 Sep 2010 at 11:15

GoogleCodeExporter commented 9 years ago 
Let's do it the cheap way for now. We'll have to review the structure of 
programming problems later anyway, once we get to helper functions, "with", 
yada yada.

Original comment by co...@strictlypositive.org on 11 Sep 2010 at 12:25

GoogleCodeExporter commented 9 years ago 
Done.

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100913120923-e29d1-e
3f7ab276047374724bc20ee63fc5f3c848ca19d.gz

Original comment by adamgundry on 13 Sep 2010 at 12:14