Notation"'rew' [ f ] e 'in' x" := (eq_rect _ f x _ e) (at level 10, x at level 10).
Definition cast_rev e : nat -> nat :=
rew [fun (T : Set) => T -> nat] eq_sym e in fun x => x.
Fail Fixpoint f (e : nat = nat) (n : nat) {struct n} := match n with
| 0 => 0
| S n => S (f e (cast_rev e n)) end. (* Problematic fixpoint : [cast_rev_e n] should not be a subterm of [n] *)
#[bypass_check(guard)] Fixpoint f (e : nat = nat) (n : nat) {struct n} := match n with
| 0 => 0
| S n => S (f e (cast_rev e n)) end.
Section Issue.
Context (e : nat = nat). (* Supposed non-trivial *)
Context (e0 : rew [fun (T : Set) => T] e in 0 = 1). (* How the non triviality may appear *)
Theorem Boom : False.
enough (f e 1 = S (f e 1)) bynowinduction (f e 1); auto. change (f e 1) with (S (f e (cast_rev e 0))) at 1.
f_equal. f_equal. apply e0'. Qed.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
