juvix/tests/positive/MicroJuvix/Implicit.mjuvix

module Implicit;

infixr 9 ∘;
∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
∘ f g x ≔ f (g x);

inductive Nat {
  zero : Nat;
  suc : Nat → Nat;
};

infixr 5 ∷;
inductive List (A : Type) {
  nil : List A;
  ∷ : A → List A → List A;
};

upToTwo : _;
upToTwo ≔ zero ∷ suc zero ∷ suc (suc zero) ∷ nil;

infixr 4 ,;
inductive Pair (A : Type) (B : Type) {
  , : A → B → Pair A B;
};

p1 : Nat → Nat → Pair Nat Nat;
p1 a b ≔ a , b ;

inductive Proxy (A : Type) {
 proxy : Proxy A;
};

t2' : {A : Type} → Proxy A;
t2' ≔ proxy;

t2 : {A : Type} → Proxy A;
t2 ≔ proxy;

t3 : ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B;
t3 _ _ ≔ proxy;

t4 : {B : Type} → Proxy B;
t4 {_} ≔ t3 proxy proxy;

t4' : {B : Type} → Proxy B;
t4' ≔ t3 proxy proxy ;

map : {A : Type} → {B : Type} → (A → B) → List A → List B;
map f nil ≔ nil;
map f (x ∷ xs) ≔ f x ∷ map f xs;

t : {A : Type} → Proxy A;
t {_} ≔ proxy;

t' : {A : Type} → Proxy A;
t' ≔ proxy;

t5 : {A : Type} → Proxy A → Proxy A;
t5 p ≔ p;

t5' : {A : Type} → Proxy A → Proxy A;
t5' proxy ≔ proxy;

f : {A : Type} → {B : Type} → A → B → _;
f a b ≔ a;

pairEval : {A : Type} → {B : Type} → Pair (A → B) A → B;
pairEval (f , x) ≔ f x;

pairEval' : {A : Type} → {B : Type} → Pair ({C : Type} → A → B) A → B;
pairEval' (f , x) ≔ f {Nat} x;

end;