search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
367 stars 79 forks source link

`tmUnquote` will normalize the term (get rid of all `tLetIn`) #1091

Open WeituoDAI opened 2 months ago

WeituoDAI commented 2 months ago

It seems that the tmUnquote will normalize the term automatically, especially get rid of all tLetIn in the term. An example:

MetaCoq Quote Definition mytp := (let x := (let y := nat in y) in x -> x).
MetaCoq Unquote Definition mytp' := mytp.
Print mytp'.

The output is mytp' = nat -> nat. Not the same as originally defined. I wonder if this is the expected behavior of the un-quotation.