def Cedar.Validation.lubBool (b₁ b₂ : BoolType) : BoolType

Equations

• Cedar.Validation.lubBool b₁ b₂ = if b₁ = b₂ then b₁ else Cedar.Validation.BoolType.anyBool

def Cedar.Validation.lubQualifiedType (q₁ q₂ : QualifiedType) : Option QualifiedType

Equations

• Cedar.Validation.lubQualifiedType (Cedar.Validation.Qualified.optional ty₁) (Cedar.Validation.Qualified.optional ty₂) = do let ty ← ty₁ ⊔ ty₂ some (Cedar.Validation.Qualified.optional ty)
• Cedar.Validation.lubQualifiedType (Cedar.Validation.Qualified.required ty₁) (Cedar.Validation.Qualified.required ty₂) = do let ty ← ty₁ ⊔ ty₂ some (Cedar.Validation.Qualified.required ty)
• Cedar.Validation.lubQualifiedType q₁ q₂ = none

def Cedar.Validation.lubRecordType (ty₁ ty₂ : List (Spec.Attr × QualifiedType)) : Option (List (Spec.Attr × QualifiedType))

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.lubRecordType [] [] = some []
• Cedar.Validation.lubRecordType ty₁ ty₂ = none

def Cedar.Validation.lub? (ty₁ ty₂ : CedarType) : Option CedarType

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Validation.CedarType.bool b₁ ⊔ Cedar.Validation.CedarType.bool b₂) = some (Cedar.Validation.CedarType.bool (Cedar.Validation.lubBool b₁ b₂))
• (s₁.set ⊔ s₂.set) = do let lub ← s₁ ⊔ s₂ some lub.set
• (ty₁ ⊔ ty₂) = if ty₁ = ty₂ then some ty₁ else none

def Cedar.Validation.subty (ty₁ ty₂ : CedarType) : Bool

Equations

• (ty₁ ⊑ ty₂) = match ty₁ ⊔ ty₂ with | some ty => decide (ty = ty₂) | none => false

def Cedar.Validation.«term_⊔_» : Lean.TrailingParserDescr

Equations

• Cedar.Validation.«term_⊔_» = Lean.ParserDescr.trailingNode `Cedar.Validation.«term_⊔_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 51))

def Cedar.Validation.«term_⊑_» : Lean.TrailingParserDescr

Equations

• Cedar.Validation.«term_⊑_» = Lean.ParserDescr.trailingNode `Cedar.Validation.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))