search

namme-anetten / epigram

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

News propagation bug with let-definitions #105

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 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