diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 18:11:51 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-30 18:11:51 +0100 |
| commit | ce12efa08f576ee2b97818a7209df328836fc638 (patch) | |
| tree | faee950920a1d810ecaf0d3a866b0acc085ec2c5 | |
| parent | 28ea499486dd17076d8f2f4c31d7fdebeacdff8e (diff) | |
[test-suite] Test section-local mutual Fixpoint.
Noticed by coverage, test code by Gäetan Gilbert.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
| -rw-r--r-- | test-suite/success/Fixpoint.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index ce3fddf249..6c333121da 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -97,8 +97,19 @@ Section visibility. Let Fixpoint by_proof (n:nat) : True. Proof. exact I. Defined. + Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool. + Proof. + - destruct n as [|n]. + + exact true. + + exact (bar n). + - destruct n as [|n]. + + exact false. + + exact (foo n). + Qed. + Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool. Admitted. + End visibility. Fail Check imm. |