errors.expected

 ￫ error[E0401]
 ￭ user-supplied term
 1 | a
   ^ term synthesized type A but is being checked against type Type

 ￫ error[E0502]
 ￭ user-supplied term
 1 | refl f a
   ^ not enough arguments for a higher-dimensional function application

 ￫ error[E0502]
 ￭ user-supplied term
 1 | refl f a a
   ^ not enough arguments for a higher-dimensional function application

 ￫ error[E0503]
 ￭ user-supplied term
 1 | Id A a
   ^ not enough arguments to instantiate a higher-dimensional type

 ￫ error[E0501]
 ￭ user-supplied term
 1 | x ↦ x
   ^ not enough non-cube variables for higher-dimensional abstraction: need 2 more

 ￫ error[E0501]
 ￭ user-supplied term
 1 | x y ↦ x
   ^ not enough non-cube variables for higher-dimensional abstraction: need 1 more

 ￫ error[E0700]
 ￭ user-supplied term
 1 | x0 x1 x2 x3 ↦ refl f x0 x1 x2
   ^ checking abstraction against non-function type refl A (f x0) (f x1)

 ￫ error[E0400]
 ￭ user-supplied term
 1 | refl (x ↦ x)
   ^ non-synthesizing term in synthesizing position (argument of degeneracy)

 ￫ error[E0600]
 ￭ user-supplied term
 1 | refl
   ^ missing argument for degeneracy refl

 ￫ error[E0601]
 ￭ user-supplied term
 1 | sym f
   ^ argument of degeneracy 'sym' must have dimension at least ee

 ￫ error[E0601]
 ￭ user-supplied term
 1 | sym a2
   ^ argument of degeneracy 'sym' must have dimension at least ee

 ￫ error[E0300]
 ￭ user-supplied term
 1 | g
   ^ unbound variable: g

 ￫ error[E0401]
 ￭ user-supplied term
 1 | a
   ^ term synthesized type A but is being checked against type refl A

 ￫ error[E0401]
 ￭ user-supplied term
 1 | a
   ^ term synthesized type
       A
     but is being checked against type
       A⁽ᵉᵉ⁾ a a (refl a) a a (refl a)

 ￫ error[E0200]
 ￭ user-supplied term
 1 | x y {` unterminated block comment‹EOF›
   ^ parse error

 ￫ error[E0200]
 ￭ user-supplied term
 1 | f (x‹EOF›
   ^ parse error

 ￫ error[E0200]
 ￭ user-supplied term
 1 | .fst x
   ^ parse error

 ￫ error[E0203]
 ￭ user-supplied term
 1 | x .fs.t y
   ^ invalid field name: .fs.t

 ￫ error[E0204]
 ￭ user-supplied term
 1 | f (con.str. x)
   ^ invalid constructor name: con.str.

 ￫ error[E0300]
 ￭ user-supplied term
 1 | x |-> f 0.1.2 x
   ^ unbound variable: 0.1.2

 ￫ error[E0202]
 ￭ user-supplied term
 1 | let x.y ≔ z in w
   ^ invalid local variable name: x.y

 ￫ error[E0202]
 ￭ user-supplied term
 1 | x.y ↦ z
   ^ invalid local variable name: x.y

 ￫ error[E0202]
 ￭ user-supplied term
 1 | a x.y b ↦ z
   ^ invalid local variable name: x.y

 ￫ error[E0200]
 ￭ user-supplied term
 1 | ↦ x
   ^ parse error

 ￫ error[E0200]
 ￭ user-supplied term
 1 | (f x) y ↦ z
   ^ parse error

 ￫ error[E0100]
 ￭ user-supplied term
 1 | _
   ^ unification arguments not yet implemented

 ￫ error[E0904]
 ￭ user-supplied term
 1 | a ↦ ( fst ≔ a, fst ≔ a )
   ^ record field 'fst' appears more than once in tuple

 ￫ error[E0905]
 ￭ user-supplied term
 1 | ( (x) ≔ a )
   ^ invalid field in tuple

 ￫ error[E0400]
 ￮ non-synthesizing term in synthesizing position (top-level unsynth)

 ￫ error[E0400]
 ￮ non-synthesizing term in synthesizing position (top-level unsynth)

 ￫ error[E0200]
 ￭ user-supplied term
 1 | [ | | .head |-> 0 | .tail |-> f ]
   ^ parse error

 ￫ error[E0902]
 ￭ user-supplied term
 1 | ( fst ≔ a )
   ^ record field 'snd' missing in tuple

 ￫ error[E0900]
 ￭ user-supplied term
 1 | ( fst ≔ a )
   ^ checking tuple against non-record type A

 ￫ error[E0900]
 ￭ user-supplied term
 1 | ( fst ≔ a )
   ^ checking tuple against non-record type ℕ

 ￫ error[E0800]
 ￭ user-supplied term
 1 | s .third
   ^ record type Σ has no field named third

 ￫ error[E1000]
 ￭ user-supplied term
 1 | zero.
   ^ non-datatype Σ A B has no constructor named zero

 ￫ error[E1000]
 ￭ user-supplied term
 1 | two.
   ^ datatype ℕ has no constructor named two

 ￫ error[E1001]
 ￭ user-supplied term
 1 | zero. a
   ^ too many arguments to constructor zero (1 extra)

 ￫ error[E1001]
 ￭ user-supplied term
 1 | suc.
   ^ not enough arguments to constructor suc (need 1 more)

 ￫ error[E0101]
 ￭ user-supplied term
 1 | 4.2
   ^ unsupported numeral: 21/5

 ￫ error[E0901]
 ￭ user-supplied term
 1 | (ungel ≔ r2)
   ^ can't check a tuple against a record Gel with a nonidentity degeneracy applied

 ￫ error[E0800]
 ￭ user-supplied term
 1 | gg' .ungel
   ^ record type with a nonidentity degeneracy applied is no longer a record, hence has no field named ungel

 ￫ error[E0506]
 ￭ user-supplied term
 1 | x ↦ x.0
   ^ invalid face: variable of dimension 0 has no face '0'