inductive Cedar.Spec.PatElem : Type

• star : PatElem
• justChar (c : Char) : PatElem

instance Cedar.Spec.instReprPatElem : Repr PatElem

Equations

• Cedar.Spec.instReprPatElem = { reprPrec := Cedar.Spec.instReprPatElem.repr }

def Cedar.Spec.instReprPatElem.repr : PatElem → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.instReprPatElem.repr Cedar.Spec.PatElem.star prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.PatElem.star")).group prec✝

instance Cedar.Spec.instDecidableEqPatElem : DecidableEq PatElem

Equations

• Cedar.Spec.instDecidableEqPatElem = Cedar.Spec.instDecidableEqPatElem.decEq

def Cedar.Spec.instDecidableEqPatElem.decEq (x✝ x✝¹ : PatElem) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqPatElem.decEq Cedar.Spec.PatElem.star Cedar.Spec.PatElem.star = isTrue ⋯
• Cedar.Spec.instDecidableEqPatElem.decEq Cedar.Spec.PatElem.star (Cedar.Spec.PatElem.justChar c) = isFalse ⋯
• Cedar.Spec.instDecidableEqPatElem.decEq (Cedar.Spec.PatElem.justChar c) Cedar.Spec.PatElem.star = isFalse ⋯
• Cedar.Spec.instDecidableEqPatElem.decEq (Cedar.Spec.PatElem.justChar a) (Cedar.Spec.PatElem.justChar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instInhabitedPatElem : Inhabited PatElem

Equations

• Cedar.Spec.instInhabitedPatElem = { default := Cedar.Spec.instInhabitedPatElem.default }

def Cedar.Spec.instInhabitedPatElem.default : PatElem

Equations

• Cedar.Spec.instInhabitedPatElem.default = Cedar.Spec.PatElem.star

instance Cedar.Spec.instCoeCharPatElem : Coe Char PatElem

Equations

• Cedar.Spec.instCoeCharPatElem = { coe := fun (c : Char) => Cedar.Spec.PatElem.justChar c }

def Cedar.Spec.PatElem.lt : PatElem → PatElem → Bool

Equations

• (Cedar.Spec.PatElem.justChar c₁).lt (Cedar.Spec.PatElem.justChar c₂) = decide (c₁ < c₂)
• Cedar.Spec.PatElem.star.lt (Cedar.Spec.PatElem.justChar c) = true
• x✝¹.lt x✝ = false

instance Cedar.Spec.instLTPatElem : LT PatElem

Equations

• Cedar.Spec.instLTPatElem = { lt := fun (x y : Cedar.Spec.PatElem) => x.lt y = true }

instance Cedar.Spec.PatElem.decLt (x y : PatElem) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

@[reducible, inline]

abbrev Cedar.Spec.Pattern : Type

Equations

• Cedar.Spec.Pattern = List Cedar.Spec.PatElem

def Cedar.Spec.wildcardMatch (text : String) (pattern : Pattern) : Bool

Equations

• Cedar.Spec.wildcardMatch text pattern = StateT.run' (Cedar.Spec.wildcardMatchIdx✝ text.toList pattern 0 0 ⋯ ⋯) ∅