diff options
Diffstat (limited to 'test-suite/bugs/closed/3886.v')
-rw-r--r-- | test-suite/bugs/closed/3886.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v new file mode 100644 index 000000000..2ac4abe54 --- /dev/null +++ b/test-suite/bugs/closed/3886.v @@ -0,0 +1,23 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). + +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) + := _ +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) + := _. +Obligations. +Axiom cheat : forall {A}, A. +Obligation 1 of doubleE. +apply cheat. +Qed. + +Obligation 1 of doubleO. +apply cheat. +Qed. + +Check doubleE.
\ No newline at end of file |