|
Require Import EquivDec List.
Generalizable All Variables.
Program Definition list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
(fun (x y : list A) => _).
Admit Obligations of list_eqdec.
Program Definition list_eqdec' `(eqa : EqDec A eq) : EqDec (list A) eq :=
(fun _ : nat => (fun (x y : list A) => _)) 0.
Admit Obligations of list_eqdec'.
¤ Dauer der Verarbeitung: 0.0 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.
|
