Seclib.Prim.Glob

toLowerStr — ⚪ definition

def · source

Vendor-neutral case folding, glob pattern matching, and string lemmas. No cloud provider noun appears in this module.

def toLowerStr (s : String) : String

matchPatternGo — ⚪ definition

def · source

def matchPatternGo (ps vs : List Char) : Bool

matchPattern — ⚪ definition

def · source

def matchPattern (pattern : String) (value : String) : Bool

ciEq — ⚪ definition

def · source

def ciEq (s₁ s₂ : String) : Bool

ciEq_toLowerStr — 🟢 proved

theorem · source

theorem ciEq_toLowerStr (s s' : String) (h : ciEq s s' = true) :
    toLowerStr s = toLowerStr s'

matchPatternGo_literal_eq — 🟢 proved

theorem · source

theorem matchPatternGo_literal_eq (ps vs : List Char)
    (hno_star : '*' ∉ ps) (hno_q : '?' ∉ ps)
    (h : matchPatternGo ps vs = true) :
    ps = vs

matchPattern_literal_mp — 🟢 proved

theorem · source

theorem matchPattern_literal_mp (p s : String)
    (hno_star : '*' ∉ p.toList) (hno_q : '?' ∉ p.toList)
    (h : matchPattern p s = true) :
    ciEq p s = true

matchPattern_cs_literal_eq — 🟢 proved

theorem · source

theorem matchPattern_cs_literal_eq (p s : String)
    (hno_star : '*' ∉ p.toList) (hno_q : '?' ∉ p.toList)
    (h : matchPattern p s = true) : p = s

toLower_eq_star — 🟢 proved

theorem · source

theorem toLower_eq_star (c : Char) (h : c.toLower = '*') : c = '*'

toLower_eq_question — 🟢 proved

theorem · source

theorem toLower_eq_question (c : Char) (h : c.toLower = '?') : c = '?'