blob: c69d31f401249da31467675dd8e49724a78b08a9 (
plain)
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
|
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
fix even_pos_odd_pos 2
with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
intros.
destruct H.
omega.
apply odd_pos_even_pos in H.
omega.
intros.
destruct H.
apply even_pos_odd_pos in H.
omega.
|
