Require Import Vector Program.
Program Definition append_nil_def :=
forall A n (ls: t A n), append ls (nil A) = ls. (* Works *)
Lemma append_nil : append_nil_def. (* Works *)
Proof.
Admitted.
Program Lemma append_nil' :
forall A n (ls: t A n), append ls (nil A) = ls.
Abort.
Fail Program Lemma append_nil'' :
forall A B n (ls: t A n), append ls (nil A) = ls.
(* Error: Anomaly "Evar ?X25 was not declared." Please report at http://coq.inria.fr/bugs/. *)
¤ Dauer der Verarbeitung: 0.15 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.
|
