# Nethra

## Terms

``````n in Ident
i in Int
c in Char

e ::=
Type_i                -- Type at level i
n                     -- Variable

C(i:e)                -- Constructor ???
i                     -- Integer literal
c                     -- Character literal

Π(n:e).e   Π{n:e}.e   -- Dependant function type
λ(n).e     λ{n}.e     -- Function
e e        e {e}      -- Application

Σ(n:e).e              -- Dependant pair type
e , e                 -- Pair
fst e                 -- Left projection
snd e                 -- Right Projection

e + e                 -- Disjunction
inl e                 -- Left injection
inr e                 -- Right injection
case e e e            -- Catamorphism

μ(n).e                -- Recursion
fold (μ(n).e) e       -- Fold recursive type
unfold (μ(n).e) e     -- Unfold recursive type

e ∈ e                 -- Term inhabits Type

?n                    -- Hole for inference
``````

## Typing rules

### Hierarchy and hypothesis

``````---------------------     ----------------
Γ ⊢ Type_i : Type_i+1     Γ, x : T ⊢ x : T
``````

### Literals and constructors

``````l ∈ int         l ∈ char
-----------     ------------     -----------------
Γ ⊢ l : int     Γ ⊢ l : char     Γ ⊢ data(n:T) : T
``````

### Dependant function type

``````Γ, x : M ⊢ N : T
----------------
Γ ⊢ Π(x:M).N : T

Γ, x : A ⊢ B : T          Γ, x : A ⊢ B : T
---------------------     ---------------------
Γ ⊢ λ(x).B : Π(x:A).T     Γ ⊢ λ{x}.B : Π{x:A}.T

Γ ⊢ f : Π(x:M).N   Γ ⊢ e : M      Γ ⊢ f : Π{x:M}.N   Γ ⊢ e : M
----------------------------      ----------------------------
Γ ⊢ f e : N[x=e]                  Γ ⊢ f {e} : N[x=e]

Γ ⊢ f : Π{x:M}.N   Γ, v:M ⊢ f {v} e : N
---------------------------------------
Γ ⊢ f e : N
``````

### Dependant pair type

``````Γ,x : A ⊢ B : T
----------------
Γ ⊢ Σ(x:A).B : T

Γ ⊢ A : M   Γ ⊢ B : N[x=A]
--------------------------
Γ ⊢ A,B : Σ(x:M).N

Γ ⊢ p : Σ(x:M).N
----------------
Γ ⊢ fst p : M

Γ ⊢ p : Σ(x:M).N
----------------------
Γ ⊢ snd p : N[x=fst p]
``````

### Disjunction

``````Γ ⊢ A : T   Γ ⊢ B : T
---------------------
Γ ⊢ A + B : T

Γ ⊢ A : M
-----------------
Γ ⊢ inl A : M + N

Γ ⊢ A : N
-----------------
Γ ⊢ inr A : M + N

Γ ⊢ a : A + B   Γ ⊢ l : A -> C   Γ ⊢ r : B -> C
-----------------------------------------------
Γ ⊢ case a l r : C
``````

### Recursion

``````Γ, x : T ⊢ A : T
----------------
Γ ⊢ μ(x).A : T

Γ ⊢ A : N[x=μ(x).N]
---------------------------
Γ ⊢ fold(μ(x).N) A : μ(x).N

Γ ⊢ A : μ(x).N
----------------------------------
Γ ⊢ unfold(μ(x).N) A : N[x=μ(x).N]
``````

### Term inhabitation

``````Γ ⊢ x : T
---------------
Γ ⊢ (x ∈ T) : T
``````

View Github