|
Set Dump Bytecode.
Set Printing Universes.
Set Printing All.
Polymorphic Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
{ pure : forall {A : Type@{d}}, A -> T A
; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
}.
Universes Uo Ua.
Eval compute in @pure@{Uo Ua}.
Global Instance Applicative_option : Applicative@{Uo Ua} option :=
{| pure := @Some
; ap := fun _ _ f x =>
match f , x with
| Some f , Some x => Some (f x)
| _ , _ => None
end
|}.
Definition foo := ap (ap (pure plus) (pure 1)) (pure 1).
Print foo.
Eval vm_compute in foo.
¤ Dauer der Verarbeitung: 0.2 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.
|
