|
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).
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
