Roberto Zunino issues

Repositories
Issues
Comments

Results 1 issues of


                                            Roberto Zunino

Anomaly: variable n unbound. (using [transparent assert])

``` coq Require Import HoTT. Goal True. Proof. assert {m:nat & True} as n. exists 0. exact tt. transparent assert (H: True). destruct n. (* Anomaly: variable n unbound. Please...