You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Here's my best effort attempt at minimizing the example:
From Equations RequireImport Equations.
Inductive Ki : Type :=
| Star : Ki.
Inductive Ty : Type :=
| VarTy : Ty
| TyFun : Ty -> Ty.
Derive NoConfusion for Ty Ki.
Inductive TyWt : Ty -> Ki -> Type :=
| TyT_One A :
TyWt A Star ->
TyWt (TyFun A) Star.
Definition F : Type := True.
Inductive Wt : Ty -> Type :=
| T_App A :
F ->
Wt (TyFun A) ->
Wt A.
Lemma regularity A (h : Wt A) : TyWt A Star.
induction h.
inversion IHh. subst.
apply H0.
Defined.
Fail Equations regularity' {A} (h : Wt A) : TyWt A Star :=
regularity' (T_App A _ ha)
with regularity' ha := { | TyT_One A h0 => h0}.
The anomaly goes away if I make one of the following modifications:
Remove F from the T_App constructor
Remove the VarTy constructor from the Ty inductive type
Replace the h0 in the last line with an underscore. Equations solves the obligation automatically but the resulting definition can't be unfolded by simp.
I'm running coq-8.19.2 and coq-equations 1.3+8.19
The text was updated successfully, but these errors were encountered:
Here's my best effort attempt at minimizing the example:
The anomaly goes away if I make one of the following modifications:
F
from theT_App
constructorVarTy
constructor from theTy
inductive typeh0
in the last line with an underscore. Equations solves the obligation automatically but the resulting definition can't be unfolded bysimp
.I'm running coq-8.19.2 and coq-equations 1.3+8.19
The text was updated successfully, but these errors were encountered: