search

mwleeds / epigram

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

inconsistent naming of variables in the context #4

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
At the end of the attached log i get a context like
...
\ xf : (m : Nat) -> < plus^1 m xf : Nat > ->
...

while "infer xf" gives

(m : Nat) -> < plus^1 m xf^1 : Nat >

which seems the correct one.

Original issue reported on code.google.com by sanzhi...@gmail.com on 8 May 2010 at 6:32

Attachments:

GoogleCodeExporter commented 9 years ago 
Thanks for reporting this! The log you attached seems to be an empty file, but 
the
problem was not difficult to reproduce. I have pushed a new implementation of 
the
"show hyps" tactic (which is run when on a programming problem, giving the 
output you
mention).

Original comment by adamgundry on 11 May 2010 at 10:11