aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/vm_univ_poly_match.v
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.