Documentation

Regex.Data.Char.Basic

max valid char

Equations

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

Instances For

def Char.increment (c : 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

Instances For

min valid char

Equations

Char.min = '\x00'

Instances For

def Char.decrement (c : 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

Instances For

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) :

theorem Char.le_max (c : Char) :

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