Properties of sorts

Induction on sorts (LSort.ind); LSort_eqb decides equality (LSort_eqb_eq, LSort_eqb_refl), which gives the DecidableEq LSort instance; the type naming a sort has no free type variables (LSort.toMonoTy_freeVars); and LMonoTy.toSort? inverts LSort.toMonoTy (LMonoTy.toSort?_toMonoTy, with LMonoTy.toSortList?_toMonoTy on lists).

theorem Lambda.LSort.ind (P : LSort → Prop) (htcons : ∀ (name : String) (args : List LSort), (∀ (x : LSort), x ∈ args → P x) → P (tcons name args)) (hbitvec : ∀ (n : Nat), P (bitvec n)) (s : LSort) : P s

Induction on sorts with the hypothesis on the arguments of a constructor stated by list membership.

theorem Lambda.LSort_eqb_eq {s1 s2 : LSort} (heq : LSort_eqb s1 s2 = true) : s1 = s2

LSort_eqb holds only of equal sorts.

theorem Lambda.LSort_eqb_refl (a : LSort) : LSort_eqb a a = true

LSort_eqb holds of every sort and itself.

@[instance_reducible]

instance Lambda.instDecidableEqLSort : DecidableEq LSort

Decidable equality of sorts, by LSort_eqb. Equality tests on sorts (==) use it, through instBEqOfDecidableEq.

Equations

• Lambda.instDecidableEqLSort a b = if h : Lambda.LSort_eqb a b = true then isTrue ⋯ else isFalse ⋯

theorem Lambda.LSort.toMonoTy_freeVars (s : LSort) : s.toMonoTy.freeVars = []

The monomorphic type naming a sort has no free type variables.

theorem Lambda.LMonoTy.toSort?_toMonoTy {t : LMonoTy} {s : LSort} : t.toSort? = some s → s.toMonoTy = t

toSort? inverts LSort.toMonoTy.

theorem Lambda.LMonoTy.toSortList?_toMonoTy {ts : List LMonoTy} {ss : List LSort} : toSort?.toSortList? ts = some ss → LSort.toMonoTy.map ss = ts

toSort?.toSortList? inverts LSort.toMonoTy.map.