blob: 7e0755d5718e33272732e76e872470282781bbe0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Program Definition test (a b : nat) : { x : nat | x = a + b } :=
((a + b) : { x : nat | x = a + b }).
Proof.
intros.
reflexivity.
Qed.
Print test.
Require Import List.
Program hd_opt (l : list nat) : { x : nat | x <> 0 } :=
match l with
nil => 1
| a :: l => a
end.
|
