def Char.max : Char

max valid char

Equations

• Char.max = { val := 1114111, valid := Char.max.proof_1 }

def Char.increment (c : Char) : Char

incr char up to max valid char Char.max

Equations

• c.increment = if h : (c.val + 1).isValidChar then { val := c.val + 1, valid := h } else c

def Char.min : Char

min valid char

Equations

• Char.min = '\x00'

def Char.decrement (c : Char) : Char

decr char to min valid char Char.min

Equations

• c.decrement = if h : (c.val - 1).isValidChar then { val := c.val - 1, valid := h } else c

theorem Char.eq_le {c1 c2 : Char} (h : c1 = c2) : c1 ≤ c2

theorem Char.lt_le {c1 c2 : Char} (h : c1 < c2) : c1 ≤ c2

theorem Char.succ_lt {c1 c2 : Char} (h : c2.val.toNat - c1.val.toNat = 1) : c1 < c2

theorem Char.min_le (c : Char) : Char.min ≤ c

theorem Char.le_max (c : Char) : c ≤ Char.max

theorem Char.one_le_of_lt {c1 c2 : Char} (h : c1 < c2) : 1 ≤ c2.val

theorem Char.toNat_eq (c : Char) : c.val.toNat.toUInt32 = c.val

theorem Char.succ_lt_lt {c1 c2 : Char} (h : 1 + c1.toNat < c2.toNat) : c1 < c2

theorem Char.succ_lt_succ_lt {c1 c2 : Char} (h : 1 + c1.toNat < c2.toNat) (hs : (c1.val + 1).isValidChar) : { val := c1.val + 1, valid := hs } < c2

theorem Char.lt_pred_le {c1 c2 : Char} (h : c1 < c2) : c1.val ≤ c2.val - 1

theorem Char.lt_succ_le {c1 c2 : Char} (h : c1 < c2) : c1.val + 1 ≤ c2.val

theorem Char.succ_add_le__pred {c1 c2 : Char} (h : 1 + c1.toNat < c2.toNat) (hs : (c1.val + 1).isValidChar) : c1.val + 1 ≤ c2.val - 1

theorem Char.incr_le_decr {c1 c2 : Char} (h : 1 + c1.toNat < c2.toNat) : c1.increment ≤ c2.decrement