blob: 14b8085496888b489887f58504242b8a503db927 (
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.
|
