coq icon indicating copy to clipboard operation
coq copied to clipboard

Published 20 hours ago • verified publisher icon HoTT

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

Open RobertoZunino opened this issue 10 years ago • 0 comments 

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 report. *)

Using assert instead works fine.

RobertoZunino avatar Sep 30 '15 12:09 RobertoZunino