blob: abe6d0fe07d9a720d5852639f63f8fd6a67ffce6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
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.
|
