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
29
30
31
32
33
34
35
36
|
grammar
T {{ hol Typ }}, S, U :: 'T_' ::= {{ com type }}
| { l1 : T1 , .. , ln : Tn } :: :: Rec {{ com record }}
G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::= {{ com type environment }}
| empty :: :: empty
formula :: formula_ ::=
| judgement :: :: judgement
| formula1 .. formulan :: :: dots
terminals :: terminals_ ::=
| \ :: :: lambda {{ tex \lambda }}
| -> :: :: arrow {{ tex \rightarrow }}
| => :: :: Arrow {{ tex \Rightarrow }}
| |- :: :: turnstile {{ tex \vdash }}
| --> :: :: red {{ tex \longrightarrow }}
| Forall :: :: forall {{ tex \forall }}
| <: :: :: subtype {{ tex <: }}
| |-> :: :: mapsto {{ tex \mapsto }}
| = :: :: eq {{ tex \!\! = \!\! }}
| : :: :: colon {{ tex \!\! : \!\! }}
defns
Jtype :: '' ::=
defn
G |- t : T :: :: Ty :: Ty_ {{ com term [[t]] has type [[T]] }} by
G|-t0:T0 .. G|-tn-1:Tn-1
------------------------------------- :: Rcd
G|- {l0=t0,..,ln-1=tn-1}:{l0:T0,..,ln-1:Tn-1}
|
