search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
47 stars 7 forks source link

News propagation bug with let-definitions #105

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
Consider the following sequence of tactics:

make A := ? : Set ;
let x : A ;
prev ;
give Set ;
relabel x ;

The relabelling fails with

Error: make:  < x : A >  is not a set.
Error: check: inferred type A of x is not Set

It seems that the term representation of the type is not getting properly 
updated by news propagation. I think the issue may be related to the use of 
out-of-scope FAKE references, where news propagation expects all references to 
follow the scoping rules.

Original issue reported on code.google.com by adamgundry on 14 Sep 2010 at 11:44