1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
match l with
| nil => nil
| a :: l0 => f a :: F A B f l0
end
: forall A B : Set, (A -> B) -> list A -> list B
let fix f (m : nat) : nat := match m with
| 0 => 0
| S m' => f m'
end in f 0
: nat
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]
|
