|
(* Automatic computing of guard in "Theorem with"; check that guard is not
computed when the user explicitly indicated it *)
Inductive T : Set :=
| v : T.
Definition f : forall (s:nat) (t:T), nat.
fix f 2.
intros s t.
refine
match t with
| v => s
end.
Defined.
Lemma test :
forall s, f s v = s.
Proof.
reflexivity.
Qed.
¤ Dauer der Verarbeitung: 0.16 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.
|
