Fixpoint.out

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 "./output/Fixpoint.v", line 57, characters 0-51:
Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default]
File "./output/Fixpoint.v", 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,default]
File "./output/Fixpoint.v", 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,default]
File "./output/Fixpoint.v", 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,default]
File "./output/Fixpoint.v", line 72, characters 0-25:
Warning: Not a truly recursive cofixpoint. [non-recursive,fixpoints,default]
File "./output/Fixpoint.v", line 75, characters 0-48:
Warning: Not a fully mutually defined cofixpoint
(a2 and a1 are not mutually dependent).
 [non-full-mutual,fixpoints,default]
File "./output/Fixpoint.v", line 91, characters 2-15:
The command has indeed failed with message:
Recursive definition of foo and bar is ill-formed.
As a mutual fixpoint:
Not enough abstractions in the definition.
The 1st recursive definition is: "?Goal".
The 2nd recursive definition is: "?Goal0".
The condition holds up to here.
File "./output/Fixpoint.v", line 96, characters 6-19:
The command has indeed failed with message:
Recursive definition of foo and bar is ill-formed.
As a mutual fixpoint decreasing on the 1st argument of foo and
1st argument of bar:
Recursive call to bar has principal argument equal to 
"0" instead of
a subterm of "n".
As a mutual fixpoint decreasing on the 1st argument of foo and
2nd argument of bar:
Recursive call to bar has principal argument equal to 
"0" instead of
a subterm of "n".
As a mutual fixpoint decreasing on the 2nd argument of foo and
1st argument of bar:
Recursive call to bar has principal argument equal to 
"0" instead of
a subterm of "m".
As a mutual fixpoint decreasing on the 2nd argument of foo and
2nd argument of bar:
Recursive call to bar has principal argument equal to 
"0" instead of a subterm of "m".
The 1st recursive definition is:
"fun n m : nat =>
 match n with
 | 0 => bar 0 0
 | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0
 end".
The 2nd recursive definition is: "fun n m : nat => ?Goal".
The condition holds up to here.
The condition holds up to here.
The condition holds up to here.
The condition holds up to here.
File "./output/Fixpoint.v", line 123, characters 6-19:
The command has indeed failed with message:
Recursive definition of foo' and bar' is ill-formed.
As a mutual fixpoint decreasing on the 1st argument of foo' and
1st argument of bar':
Fixpoints on proof irrelevant inductive types should produce proof irrelevant
values.
As a mutual fixpoint decreasing on the 1st argument of foo' and
2nd argument of bar':
Recursive call to bar' has principal argument equal to 
"0" instead of a subterm of "n".
The 1st recursive definition is:
"fun (n : nat) (m : Prop) =>
 match n with
 | 0 => bar' SI 0
 | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0
 end".
The 2nd recursive definition is: "fun (n : STrue) (m : nat) => ?Goal".