ProgramDefinition 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).
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.
