Lem User’s Manual:
version 0.2

Lem is a lightweight tool for writing, managing, and publishing large scale semantic definitions. It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems (such as Coq, HOL4, and Isabelle).

It resembles a pure subset of Objective Caml, supporting typical functional programming constructs, including top-level parametric polymorphism, datatypes, records, higher-order functions, and pattern matching. It also supports common logical mechanisms including list and set comprehensions, universal and existential quantifiers, and inductively defined relations. From this, Lem generates OCaml, HOL4 and Isabelle code; the OCaml backend uses a finite set library (and does not yet support inductive relations). A Coq backend is in development.

This is a preliminary release of Lem which is not yet feature complete (see Section 5). It is currently released under a restrictive license, but we intend to use an open source or free software license release for later, more complete releases.

1  Installing Lem

Lem depends on OCaml (http://caml.inria.fr/), and the Batteries Included library (http://batteries.forge.ocamlcore.org/) Batteries Included in turn depends on findlib (http://projects.camlcity.org/projects/findlib.html) and Camomile (http://camomile.sourceforge.net/). Lem is tested against OCaml 3.12.1, Batteries Included 1.4.0, findlib 1.2.7 and Camomile 0.8.3. Earlier versions have a good chance of working, but not OCaml prior to 3.12.0.

To build Lem run make in Lem’s top-level directory. This builds the executable lem, and places a symbolic link to it in Lem’s root directory. Now set the LEMLIB environment variable to path_to_lem/library, or alternately pass the -lib path_to_lem/library flag to lem when you run it. This tells Lem where to find its library of types for HOL/Isabelle/OCaml/Coq built-in functions.

2  Invoking Lem

Lem processes and type checks its .lem file arguments in order. Each of the -hol, -isa, -tex, -coq, and -ocaml flags cause Lem to produce output for the corresponding system, one output file per input file. For example,

lem name1.lem name2.lem -ocaml -hol -isa 

creates 6 files (assuming there are no type errors in the source files), name1.ml, name2.ml, Name1Script.sml, Name2Script.sml, Name1.thy, and Name2.thy.

Lem-generated OCaml relies on the files in ocaml_lib, and so they must be compiled to link with path_to_lem/ocaml-lib/_build/extract.cma (or extract.cmxa). For example,

ocamlc -I path_to_lem/ocaml-lib/_build -o name extract.cma name1.ml

If the -tex option is specified, then for each input file name.lem the tool will create both a stand-alone LaTeX file name.tex that typesets the whole of that file and a file name-inc.tex of LaTeX definitions, one for each top-level Lem definition, that can be included in the preamble of another document, so that particular top-level Lem definitions can be quoted within it. Additionally, Lem will create a single alldoc.tex and alldoc-inc.tex with the content of all the Lem input files. Lem-generated L^AT_EX makes use of macros defined in path_to_lem/tex-lib/lem.sty.

3  Syntax

Lem generally follows the syntax of the pure functional fragment of OCaml, with the following notable differences:

• curried constructors, e.g.,

  type t = C of num * bool
  let x = C 1 2
  

• <| and |> surround record expressions.
• match and function must terminate with the keyword end.
• All names can begin with either upper or lower case letters (except for module names, which must be capitalised).
• Lem supports list and set comprehensions, inductive relations, type classes, and universal and existential quantification.

3.1  Literals

A literal constant lit is either

• true
  false
  booleans constants
• ( )
  the unit constant
• a (non-empty) sequence of digits
  a numeric constant
• a sequence of non-" characters surrounded by "
  a string constant

3.2  Variables and other names

A name x is a non-empty sequence of characters starting with a letter or the _ character, followed by letters, numbers and the _ and ’ characters.

An identifier   id   is a non-empty sequence of names separated by the . character. An identifier is a module path, so all but the last name must refer to modules, and hence begin with capital letters.

A constructor name C is an identifier that refers to the definition of a data constructor.

A field name fn is an identifier that refers to a field of a defined record type.

An infix name ix is a non-empty sequence of symbolic characters: !$%&*+-./:<=>?@|~^ (except for sequences that are otherwise used as keywords, such as ->).

Infix operators are parsed in precedence on their first character in the following order, from tightest binding to weakest:

• **
• * and / and % (also inter)
• + and - (also union)
• (also ::)
• @ and ^
• = and < and > and | and & and $ (also IN and MEM and subset and \)
• &&
• ||
• -->

3.3  Patterns

As in OCaml, most binding forms in Lem use patterns which match against a value and can bind multiple names to various of its sub-values.

A pattern pat is either

• lit
  a literal pattern; matches the given literal constant
•   _  
  the wildcard pattern; matches anything
• x
  a variable pattern; matches anything and binds it to the variable x
• C
  a constant constructor pattern; matches the constructor C
• C   pat₁   ...   pat_n
  a constructor pattern; matches the n argument constructor C if its arguments match the sub-patterns
• ( pat₁ ,   ...   , pat_n ) where n ≥ 2
  a tuple pattern; matches an n-tuple whose components match the sub-patterns
• [ pat₁ ;   ...   ; pat_n   ;^? ]
  a list pattern; matches an n-element list whose components match the sub-patterns (the closing ; is optional)
• [   ] the empty list pattern; matches the empty list
• pat₁ :: pat₂
  a list pattern; matches a non-empty list whose head matches pat₁ and whose tail matches pat₂
• ⟨| fn₁ = pat₁ ;   ...   ; fn_n = pat_n   ;^? |⟩
  a record pattern; matches a record with the given fields whose contents match the sub-patterns (some of the records fields can be omitted, but none can be duplicated; the closing ; is optional)
• ( pat : typ )
  a type-annotated pattern; requires that pat matches values of type   typ
• pat   as   x  
  an as pattern; matches values that match the sub-pattern and also bind the value to the variable x
• ( pat )
  a parenthesized pattern, the same as pat

3.4  Expressions

An expression exp is either

• lit
  a literal constant
•   id  
  an identifier
• fun   pat₁   ...   pat_n → exp  
  an n-argument function; the patterns must be able to match any value of their type, and their bindings are bound in the function’s body exp
• function   |^?   pat₁ → exp₁   ∣   ...   ∣ pat_n → exp_n     end
  a single-argument function; each pat_i’s variables are bound in the corresponding exp_i, and the function’s argument is matched against the patterns (the initial | is optional)
• exp₁   exp₂
  a function application
• exp₁   ix     exp₂
  an infix operation
• match   exp   with   |^?   pat₁ → exp₁   ∣   ...   ∣ pat_n → exp_n       end
  a match expression; each pat_i’s variables are bound in the corresponding exp_i, and the given exp is matched against the patterns (the initial | is optional)
• if   exp₁   then   exp₂   else   exp₃
  a conditional
• C
  a data constructor
• [ exp₁ ;   ...   ; exp_n   ;^? ]
  an n-element list (the closing ; is optional)
• [   ]
  the empty list
• exp1::exp2
  a list; with exp₁ at the head
• ( exp₁ ,   ...   , exp_n ) where n ≥ 2
  an n-tuple
• ⟨| fn₁ = exp₁   ;   ...   ; fn_n = exp_n     ;^?   |⟩
  a record expression; the field names can appear in any order, but must not be duplicated, and must contain exactly the fields from the record’s type definition (the closing ; is optional)
• ⟨| exp   with   fn₁ = exp₁   ;   ...   ; fn_n = exp_n     ;^?   |⟩ a record update expression; the field names must be a subset of the record’s fields, and not duplicate (the closing ; is optional)d
• exp . fn field projection; get the given field’s value from a record
• ( exp : typ )
  a type annotation; requires exp to have type   typ
• let   pat   = exp₁     in   exp₂
  let   pat   : typ = exp₁     in   exp₂
  locally bind the variables of pat in exp₂; pat must be able to match any value of its type, which in the latter form must be   typ
• let   x     pat₁   ...   pat_n   = exp₁     in   exp₂
  let   x     pat₁   ...   pat_n   : typ = exp₁     in   exp₂
  locally bind the n-argument function x in exp₂; each pat_i must be able to match any value of its type, and their variables are bound in exp₁
• {   }
  the empty set
• a set whose elements are given by the sub-expressions, which can be duplicate values (the closing ; is optional)
• { exp₁ ∣ exp₂ }
  a set comprehension; the comprehension ranges over the free variables of exp₁ that are not bound by the enclosing scope
• { exp₁ ∣   forall   qbind₁   ...   qbind_n ∣ exp₂ }
  a set comprehension; it ranges over the variables in the quantification bindings (see below)
• [ exp₁ ∣   forall   qbind₁   ...   qbind_n ∣ exp₂ ]
  a list comprehension; it ranges over the variables in the quantification bindings (see below), which must not be restricted over sets
• forall   qbind₁   ...   qbind_n . exp
  exist   qbind₁   ...   qbind_n . exp
  quantification (see below on quantification bindings)
• begin   exp   end
  ( exp )
  grouping; the same as exp

Quantification bindings support quantifying over and comprehending over a restricted domain. In a list of quantification bindings, no variable can be appear twice as a binder; however, later expressions can refer to earlier bindings. If a given pattern does not match all variables, then in a comprehension or forall context they are ignored. In an exist context, the witness must match the pattern.

A quantification binding qbind is either

• x
  a variable
• ( pat   IN   exp )
  restricted quantification over a set
• ( pat   MEM   exp )
  restricted quantification over a list

3.5  Definitions

Several of the definition forms are parameterized by an optional target_opt that specifies a set of targets that the definition should be used for. This allows different definitions of a particular function to be used for the different targets.

3.5.1  Type definitions

Lem supports the definition of algebraic datatypes, record types, and type abbreviations. Each top-level type definition is a sequence of type definition expressions td:
type   td₁   and   ...   and   td_n
where a type definition expression td is either

• tyvars   x   = |^?   ctor_def₁ ∣   ...   ∣ ctor_def_n
  an algebraic type with n constructors/variants; each constructor definition ctor_def_n can refer to the tyvars (the initial | is optional)
• tyvars   x   = ⟨| x₁   : typ₁ ;   ...   ; x_n   : typ_n   ;^? |⟩
  a record type; each typ_i can refer to the tyvars (the closing ; is optional)
• tyvars   x   = typ
  a type abbreviation;   typ can refer to the tyvars
• tyvars   x  
  an abstract type abbreviation

A constructor definition   ctor_def is either

• x
  a constant constructor
• x     of   typ₁ *   ...   * typ_n
  an n-argument constructor, which is treated as an n-argument curried function

tyvars is either

• 
  no type variables
• ’ x
  a single type variable
• ( ’ x₁ ,   ...   , ’ x_n ) where n ≥ 2
  a list of type variables

3.5.2  Inductive relations

An inductive relation is defined with a sequence of rules
indreln   targets^?   rule₁   and   ...   and   rule_n
where each rule_i is

• forall   x₁     ...   x_k   . exp =⇒ x     exp₁   ...   exp_n
  defines the n-ary relation x to hold of the exp_i when exp holds.

3.5.3  Other definitions

A definition is either

• a type definition (Section 3.5.1)
• let   targets^?   pat   = exp  
  let   targets^?   pat   : typ = exp  
  
• let   rec   targets^?   funcl₁   and   ...   and   funcl_n
  
• an inductively defined relation (Section 3.5.2)
  
• val   x   :   typ
  val   x   : forall   ’ x₁     ...   ’ x_n   .   typ
  val   x   : forall   ’ x₁     ...   ’ x_n   . ( id₁   ’ y₁   )   ...   ( id_k   ’ y_k   ) ⇒   typ
  a type specification for the name x; further definitions of x must have the given type
• class   ( x     ’ y   )   val   x₁   : typ₁     ...   val   x_n   : typ_n     end
  
• instance   instschm   val_def₁     ...   val_def_n     end
  
• module   x   =   struct   defs   end
  
• module   x   = id
  
• open   id
  
• sub   [ target ] x     x₁     ..   x_n   = exp
  

3.6  Types

A   typ is either:

• ’ x
  
• typ₁ → typ₂
  
• typ₁ *   ...   * typ_n when n ≥ 2
  
• ( typ₁ ,   ...   , typ_n ) id when n ≥ 2
  
•   typ   id  
  
•   id  
  
•   ( typ )  
  

4  Libraries

4.1  Pervasives

4.2  List

4.3  Set

4.4  Pmap

5  Status

5.1  Working features

• Typechecking for the the entire Lem input language
• HOL, Isabelle/HOL, and OCaml backends (except as noted in Section 5.2).
• L^AT_EX backend (partial)

5.2  Features in development

• the Coq backend
• the L^AT_EX backend (although it’s somewhat usable now)
• in the OCaml backend, sets whose elements can contain functions, sets, or finite maps
• in the OCaml backend, inductive relations
• in all backends, robust checking that the generated output is valid in the target
• in all backends, type classes
• in the parse and type checker, improved error messages
• translation between the OCaml-style and HOL-style function definitions
  e.g.,

  let rec length l = match l with
    | [] -> 0
    | x::y = 1 + length l
  

  and

  let rec length [] = 0
      and length x::y = 1 + length l
  

• more robust unparsing for the various targets
• a type substitution mechanism

6  Formal syntax

The l decorations on the grammar correspond to where the implementation records source type information; they cannot appear in source programs.

---

l		::=			Source locations
		|
xl , yl , zl		::=			Location-annotated names
		|	x   l
		|	( ix ) l			Remove infix status
ixl		::=			Location-annotated infix names
		|	ix   l
		|	‵ x ‵ l			Add infix status
α		::=			Type variables
		|	’ x
αl		::=			Location-annotated type variables
		|	α   l
id		::=			Long identifers
		|	x1l .   ..   xnl . xl   l
tyvars		::=			Type variable lists
		|	( α1l ,   ..   , αnl )			Must have >1 type variables
		|	αl	S
		|		S
typ_aux		::=			Types
		|	_			Unspecified type
		|	αl			Type variables
		|	typ1 → typ2			Function types
		|	typ1 *   ....   * typn			Tuple types
		|	( typ1 ,   ..   , typn ) id			Type applications, must have >1 type arguments
		|	typ   id	S		Type applications (single argument)
		|	id	S		Type applications (no argument)
		|	( typ )
typ		::=			Location-annotated types
		|	typ_aux   l
lit_aux		::=			Literal constants
		|	true
		|	false
		|	num
		|	string
		|	( )
lit		::=
		|	lit_aux   l			Location-annotated literal constants
;?		::=			Optional semi-colons
		|
		|	;
pat_aux		::=			Patterns
		|	_			Wildcards
		|	pat   as   xl			Named patterns
		|	( pat : typ )			Typed patterns
		|	id   pat1   ..   patn			Single variable and constructor patterns
		|	⟨| fpat1 ;   ...   ; fpatn   ;? |⟩			Record patterns
		|	( pat1 ,   ....   , patn )			Tuple patterns
		|	[ pat1 ;   ..   ; patn   ;? ]			List patterns
		|	( pat )
		|	pat1 :: pat2			Cons patterns
		|	lit			Literal constant patterns
pat		::=			Location-annotated patterns
		|	pat_aux   l
fpat		::=			Field patterns
		|	id = pat   l
|?		::=			Optional bars
		|
		|	∣
exp_aux		::=			Expressions
		|	id			Identifiers
		|	fun   psexp			Curried functions
		|	function   |?   pexp1 ∣   ...   ∣ pexpn   end			Functions with pattern matching
		|	exp1   exp2			Function applications
		|	exp1   ixl   exp2			Infix applications
		|	⟨| fexps |⟩			Records
		|	⟨| exp   with   fexps |⟩			Functional update for records
		|	exp . id			Field projection for records
		|	match   exp   with   |?   pexp1 ∣   ...   ∣ pexpn   l   end			Pattern matching expressions
		|	( exp : typ )			Type-annotated expressions
		|	let   letbind   in   exp			Let expressions
		|	( exp1 ,   ....   , expn )			Tuples
		|	[ exp1 ;   ..   ; expn   ;? ]			Lists
		|	( exp )
		|	begin   exp   end			Alternate syntax for (exp)
		|	if   exp1   then   exp2   else   exp3			Conditionals
		|	exp1 :: exp2			Cons expressions
		|	lit			Literal constants
		|	{ exp1 ∣ exp2 }			Set comprehensions
		|	{ exp1 ∣   forall   qbind1   ..   qbindn ∣ exp2 }			Set comprehensions with explicit binding
		|	{ exp1 ;   ..   ; expn   ;? }			Sets
		|	q   qbind1   ...   qbindn . exp			Logical quantifications
		|	[ exp1 ∣   forall   qbind1   ..   qbindn ∣ exp2 ]			List comprehensions (all binders must be quantified)
exp		::=			Location-annotated expressions
		|	exp_aux   l
q		::=			Quantifiers
		|	forall
		|	exist
qbind		::=			Bindings for quantifiers
		|	xl
		|	( pat   IN   exp )			Restricted quantifications over sets
		|	( pat   MEM   exp )			Restricted quantifications over lists
fexp		::=			Field-expressions
		|	id = exp   l
fexps		::=			Field-expression lists
		|	fexp1 ;   ...   ; fexpn   ;?   l
pexp		::=			Pattern matches
		|	pat → exp   l
psexp		::=			Multi-pattern matches
		|	pat1   ...   patn → exp   l
tannot?		::=			Optional type annotations
		|
		|	: typ
funcl_aux		::=			Function clauses
		|	xl   pat1   ...   patn   tannot? = exp
letbind_aux		::=			Let bindings
		|	pat   tannot? = exp			Value bindings
		|	funcl_aux			Function bindings
letbind		::=			Location-annotated let bindings
		|	letbind_aux   l
funcl		::=			Location-annotated function clauses
		|	funcl_aux   l
rule_aux		::=			Inductively defined relation clauses
		|	forall   x1l   ..   xnl . exp =⇒ xl   exp1   ..   expi
rule		::=			Location-annotated inductively defined relation clauses
		|	rule_aux   l
typs		::=			Type lists
		|	typ1 *   ...   * typn
ctor_def		::=			Datatype definition clauses
		|	xl   of   typs
		|	xl	S		Constant constructors
texp		::=			Type definition bodies
		|	typ			Type abbreviations
		|	⟨| x1l : typ1 ;   ...   ; xnl : typn   ;? |⟩			Record types
		|	|?   ctor_def1 ∣   ...   ∣ ctor_defn			Variant types
td		::=			Type definitions
		|	tyvars   xl = texp
		|	tyvars   xl			Definitions of opaque types
c		::=			Typeclass constraints
		|	( id   αl )
cs		::=			Typeclass constraint lists
		|
		|	c1   ..   ci ⇒			Must have >0 constraints
c_pre		::=			Type and instance scheme prefixes
		|
		|	forall   α1l   ..   αnl . cs			Must have >0 type variables
typschm		::=			Type schemes
		|	c_pre   typ
instschm		::=			Instance schemes
		|	c_pre ( id   typ )
target		::=			Backend target names
		|	hol
		|	isabelle
		|	ocaml
		|	coq
		|	tex
targets		::=			Backend target name lists
		|	{ target1 ;   ...   ; targetn }
targets?		::=			Optional targets
		|
		|	targets
val_def		::=			Value definitions
		|	let   targets?   letbind			Non-recursive value definitions
		|	let   rec   targets?   funcl1   and   ...   and   funcln			Recursive function definitions
val_spec		::=			Value type specifications
		|	val   xl : typschm
def_aux		::=			Top-level definitions
		|	type   td1   and   ...   and   tdn			Type definitions
		|	val_def			Value definitions
		|	module   xl =   struct   defs   end			Module definitions
		|	module   xl = id			Module renamings
		|	open   id			Opening modules
		|	indreln   targets?   rule1   and   ...   and   rulen			Inductively defined relations
		|	val_spec			Top-level type constraints
		|	sub   [ target ] xl   x1l   ..   xil = exp			Target-specific functions to inline
		|	class   ( xl   αl )   val   x1l : typ1   l1   ...   val   xnl : typn   ln   end			Typeclass definitions
		|	instance   instschm   val_def1   l1   ...   val_defn   ln   end			Typeclass instantiations
def		::=			Location-annotated definitions
		|	def_aux   l
;;?		::=			Optional double-semi-colon
		|
		|	;;
defs		::=			Definition sequences
		|	def1   ;;1?   ..   defn   ;;n?

---

7  Formal type system

---

p		::=			Unique paths
		|	x1 .   ..   xn . x
		|	__list
		|	__bool
		|	__num
		|	__set
		|	__string
		|	__unit
σ		::=			Type variable substitutions
		|	{ α1 ↦ t1   ..   αn ↦ tn }
t , u		::=			Internal types
		|	α
		|	t1 → t2
		|	t1 *   ....   * tn
		|	t_args   p
		|	σ ( t )	M		Multiple substitutions
		|	curry   ( t_multi , t )	M		Curried, multiple argument functions
t_args		::=			Lists of types
		|	( t1 ,   ..   , tn )
		|	σ ( t_args )	M		Multiple substitutions
t_multi		::=			Lists of types
		|	( t1 *   ..   * tn )
		|	σ ( t_multi )	M		Multiple substitutions
tvs		::=			Type variable lists
		|	α1   ..   αn
names		::=			Sets of names
		|	{ x1 ,   ..   , xn }
C		::=			Typeclass constraint lists
		|	( p1   α1 )   ..   ( pn   αn )
v_desc		::=			Value descriptions
		|	⟨   forall   tvs . t_multi → p , ( x   of   names ) ⟩			Constructors
		|	⟨   forall   tvs . p → t , ( x   of   names ) ⟩			Fields
		|	forall   tvs . C ⇒ t			Values
kind		::=			Sorts of value bindings
		|	ctor
		|	field
		|	mthd
		|	let
		|	spec
		|	target
κ		::=
		|	{ kind1 ;   ..   ; kindn }
		|	κ1   ∪   κ2	M
Σ		::=			Typeclass constraints
		|	{ ( p1   t1 ) ,   ..   , ( pn   tn ) }
		|	Σ1   ∪   ..   ∪   Σn	M
E		::=			Environments
		|	⟨ Em , Ep , Ex ⟩
		|	E1 ⊎ E2	M
		|	є	M
Ex		::=			Value environments
		|	{ x1 ↦ κ1   v_desc1 ,   ..   , xn ↦ κn   v_descn }
		|	E1x ⊎   ..   ⊎ Enx	M
Em		::=			Module environments
		|	{ x1 ↦ E1 ,   ..   , xn ↦ En }
Ep		::=			Path environments
		|	{ x1 ↦ p1 ,   ..   , xn ↦ pn }
		|	E1p ⊎   ..   ⊎ Enp	M
El		::=			Lexical bindings
		|	{ x1 ↦ t1 ,   ..   , xn ↦ tn }
		|	E1l ⊎   ..   ⊎ Enl	M
tc_abbrev		::=			Type abbreviations
		|	. t
		|
tc_def		::=			Type and class constructor definitions
		|	tvs   tc_abbrev			Type constructors
Δ		::=			Type constructor definitions
		|	{ p1 ↦ tc_def1 ,   ..   , pn ↦ tc_defn }
		|	Δ1 ⊎ Δ2	M
δ		::=			Typeclass definitions
		|	{ p1 ↦ xs1 ,   ..   , pn ↦ xsn }
		|	δ1 ⊎ δ2	M
inst		::=			A typeclass instance, t must not contain nested types
		|	C ⇒ ( p   t )
I		::=			Global instances
		|	{ inst1 ,   ..   , instn }
		|	I1   ∪   I2	M
D		::=			Global type definition store
		|	⟨ Δ , δ , I ⟩
		|	D1 ⊎ D2	M
		|	є	M
xs		::=
		|	x1   ..   xn
formula		::=
		|	judgement
		|	formula1    ..    formulan
		|	Em ( x )   ▷   E			Module lookup
		|	Ep ( x )   ▷   p			Path lookup
		|	Ex ( x )   ▷   κ   v_desc			Value lookup
		|	El ( x )   ▷   t			Lexical binding lookup
		|	Δ ( p )   ▷   tc_def			Type constructor lookup
		|	δ ( p )   ▷   xs			Type constructor lookup
		|	dom   ( E1m )   ∩   dom   ( E2m ) =   ∅
		|	dom   ( E1x )   ∩   dom   ( E2x ) =   ∅
		|	dom   ( E1p )   ∩   dom   ( E2p ) =   ∅
		|	disjoint   doms   ( E1l ,   ..   , Enl )			Pairwise disjoint domains
		|	disjoint   doms   ( E1x ,   ..   , Enx )			Pairwise disjoint domains
		|	compatible   overlap   ( { x1 ↦ t1 } ,   ..   , { xn ↦ tn } )			(xi = xj) =⇒ (ti = tj)
		|	duplicates   ( tvs ) =   ∅
		|	duplicates   ( x1 ,   ..   , xn ) =   ∅
		|	x   ∉   dom   ( El )
		|	x   ∉   dom   ( Ex )
		|	p   ∉   dom   ( δ )
		|	p   ∉   dom   ( Δ )
		|	kind   ∉   κ
		|	kind ∈ κ
		|	κ1   ∩   κ2 =   ∅
		|	κ1   ≠   κ2
		|	FV   ( t )   ⊂   tvs			Free type variables
		|	FV   ( t_multi )   ⊂   tvs			Free type variables
		|	FV   ( C )   ⊂   tvs			Free type variables
		|	inst   IN   I
		|	( p   t )   ∉   I
		|	E1l = E2l
		|	E1x = E2x
		|	E1 = E2
		|	Δ1 = Δ2
		|	δ1 = δ2
		|	I1 = I2
		|	names1 = names2
		|	t1 = t2
		|	σ1 = σ2
		|	p1 = p2
		|	xs1 = xs2
		|	tvs1 = tvs2

---

tyvars ↝ tvs   

E₁ ( x₁^l   ..   x_n^l )   ▷   E₂   Name path lookup

E₁ ( id )   ▷   E₂   Module identifier lookup

E ( id )   ▷   p   Path identifier lookup

E ( id )   ▷   κ   v_desc   Value identifier lookup

Δ ⊢ t   ok   Well-formed types

Δ ⊢ t₁ = t₂   Type equality

Δ , E ⊢ typ ↝ t   Convert source types to internal types

Δ , E ⊢ typs ↝ t_multi   

⊢ lit : t   Typing literal constants

Δ , E ⊢   field   id : t_args   p → t   ▷   ( x   of   names )   Field typing (also returns canonical field names)

Δ , E ⊢   ctor   id : t_multi → t_args   p   ▷   ( x   of   names )   Data constructor typing (also returns canonical constructor names)

Δ , E ⊢   val   id : t   ▷   Σ   Typing top-level bindings, collecting typeclass constraints

E , E^l ⊢ x   not   ctor   v is not bound to a data constructor

E^l ⊢ id   not   shadowed   id is not lexically shadowed

Δ , E , E₁^l ⊢ pat : t   ▷   E₂^l   Typing patterns, building their binding environment

Δ , E , E₁^l ⊢ pat_aux : t   ▷   E₂^l   Typing patterns, building their binding environment