diff options
| author | Pierre-Marie Pédrot | 2019-10-30 23:25:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-30 23:25:25 +0100 |
| commit | c907ed752e573a57518ffc5ea05807d0e7b3c453 (patch) | |
| tree | 4df655ecbce5003068e290ef500c7897cdddbe95 | |
| parent | 55446694781674f4d4e74546fde54f3dbdea27bc (diff) | |
| parent | ce12efa08f576ee2b97818a7209df328836fc638 (diff) | |
Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.
Reviewed-by: ppedrot
| -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. |