Gépelési szabályok
"Star"
  # : #1
|
Variable
|
A:s
|
|
, x : A x : A
|
Apply
|
f : (x::A) -> B
|
a : A
|
|
f a : B[x:=a]
|
|
Lambda
|
, x : A b : B
|
((x::A) -> B) : t
|
|
(\(x::A) -> b) : ((x::A) -> B)
|
|
Pi
|
A:s
|
, x : A B : t
|
|
((x::A) -> B) : t
|
|
Conversion
|
a:A
|
B:s
|
A =ß B |
|
a : B
|
||
Weakening
|
b : B
|
B : s
|
|
, x : B b : B
|
|
Data
|
Aij : #
|
|
k > 0, nk  0
|
|
|
data
C1 A11 ... A1n1
| ... |
Ck Ak1 ... Aknk
: #
|
Constructor
T
data
C1 A11 ... A1n1
| ... |
Ck Ak1 ... Aknk
|
T : #
|
|
Ci @ T :
Ai1 -> ... -> Aiki -> T
|
Case
|
|
|
|
Product
|
A1 : s1
|
... |
An : sn
|
... |
ej : Aj
|
sig { l1 :: A1  1; ...
lk :: Ak k; ...
ln :: An n }
: #u
|
||||
i is either empty
or "= ei".where j belongs to a subset of 1..n.
Record
|
|
|
|
Select
|
|
|
|
Beta
| (\(x::A) -> B) C =ß B[x := C] |
Sel
| { l1 :: A1 = e1; ... ln :: An = en } . lk =ß ek[l1 := e.l1, ... ln := e.ln] |
Sel-Type
|
e : { l1 :: A1 1; ...
lk :: Ak = ek; ...
ln :: An n }
|
| e . lk =ß ek[l1 := e.l1, ... lb := e.ln] |
i is either empty
or "= ei".