|
Require Import Program.
Set Implicit Arguments.
Unset Strict Implicit.
Definition def (a : nat) := a = a.
Structure record {a : nat} {D : def a} :=
inR { prop : Prop }.
Program
Canonical Structure ins (a : nat) (rec : @record a _) :=
@inR a _ (prop rec).
Next Obligation.
exact eq_refl.
Defined.
Next Obligation.
exact eq_refl.
Defined.
¤ 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.
|
