diff options
Diffstat (limited to 'test-suite/output/Fixpoint.out')
| -rw-r--r-- | test-suite/output/Fixpoint.out | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 60bc9cbf55..ff7918b4e6 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -12,3 +12,27 @@ let fix f (m : nat) : nat := match m with Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1) = cofix inf : Inf := {| projS := inf |} : Inf +File "stdin", line 57, characters 0-51: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +File "stdin", line 60, characters 0-103: +Warning: Not a fully mutually defined fixpoint +(k1 depends on k2 but not conversely). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] +File "stdin", line 62, characters 0-106: +Warning: Not a fully mutually defined fixpoint +(l2 and l1 are not mutually dependent). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] +File "stdin", line 64, characters 0-103: +Warning: Not a fully mutually defined fixpoint +(m2 and m1 are not mutually dependent). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] +File "stdin", line 72, characters 0-25: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +File "stdin", line 75, characters 0-48: +Warning: Not a fully mutually defined fixpoint +(a2 and a1 are not mutually dependent). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] |