Require Program.Tactics.
Axiom foo : nat -> Prop.
Axiom fooP : forall n, foo n.
Class myClass (A: Type) :=
{
bar : A -> Prop
}.
Program Instance myInstance : myClass nat :=
{
bar := foo
}.
Class myClassP (A : Type) :=
{
super :> myClass A;
barP : forall (a : A), bar a
}.
Instance myInstanceP : myClassP nat :=
{
barP := fooP
}.
¤ 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.
|