blob: 676b97878fb48c00592807174bb61e7a208f98aa (
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
26
27
28
|
Require Program.
Obligation Tactic := idtac.
Set Shrink Obligations.
Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit :=
let bar : {r | n < r} := _ in
let qux : {r | p < r} := _ in
let quz : m = n -> True := _ in
tt.
Next Obligation.
intros m p n q.
exists (S n); constructor.
Qed.
Next Obligation.
intros m p n q.
exists (S (S m)); constructor.
Qed.
Next Obligation.
intros m p n q ? ? H.
destruct H.
constructor.
Qed.
Check (foo_obligation_1 : forall n, {r | n < r}).
Check (foo_obligation_2 : forall m, {r | (S m) < r}).
Check (foo_obligation_3 : forall m n, m = n -> True).
|
