This file defines the types of Cedar Terms. See Term.lean for the definition of the Term language.

inductive Cedar.SymCC.TermPrimType : Type

• bool : TermPrimType
• bitvec (n : Nat) : TermPrimType
• string : TermPrimType
• entity (ety : Spec.EntityType) : TermPrimType
• ext (xty : Validation.ExtType) : TermPrimType

inductive Cedar.SymCC.TermType : Type

• prim (pty : TermPrimType) : TermType
• option (ty : TermType) : TermType
• set (ty : TermType) : TermType
• record (rty : Data.Map Spec.Attr TermType) : TermType

@[reducible, inline]

abbrev Cedar.SymCC.TermType.bool : TermType

Equations

• Cedar.SymCC.TermType.bool = Cedar.SymCC.TermType.prim Cedar.SymCC.TermPrimType.bool

@[reducible, inline]

abbrev Cedar.SymCC.TermType.bitvec (n : Nat) : TermType

Equations

• Cedar.SymCC.TermType.bitvec n = Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.bitvec n)

@[reducible, inline]

abbrev Cedar.SymCC.TermType.string : TermType

Equations

• Cedar.SymCC.TermType.string = Cedar.SymCC.TermType.prim Cedar.SymCC.TermPrimType.string

@[reducible, inline]

abbrev Cedar.SymCC.TermType.entity (ety : Spec.EntityType) : TermType

Equations

• Cedar.SymCC.TermType.entity ety = Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.entity ety)

@[reducible, inline]

abbrev Cedar.SymCC.TermType.ext (xty : Validation.ExtType) : TermType

Equations

• Cedar.SymCC.TermType.ext xty = Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.ext xty)

@[reducible, inline]

abbrev Cedar.SymCC.TermType.tagFor (ety : Spec.EntityType) : TermType

Equations

• Cedar.SymCC.TermType.tagFor ety = Cedar.SymCC.TermType.record (Cedar.SymCC.EntityTag.mk (Cedar.SymCC.TermType.entity ety) Cedar.SymCC.TermType.string)

@[inline]

def Cedar.SymCC.TermType.isPrimType : TermType → Bool

Equations

• (Cedar.SymCC.TermType.prim pty).isPrimType = true
• x✝.isPrimType = false

@[inline]

def Cedar.SymCC.TermType.isEntityType : TermType → Bool

Equations

• (Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.entity ety)).isEntityType = true
• x✝.isEntityType = false

@[inline]

def Cedar.SymCC.TermType.isBitVecType : TermType → Bool

Equations

• (Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.bitvec n)).isBitVecType = true
• x✝.isBitVecType = false

@[inline]

def Cedar.SymCC.TermType.isRecordType : TermType → Bool

Equations

• (Cedar.SymCC.TermType.record rty).isRecordType = true
• x✝.isRecordType = false

@[inline]

def Cedar.SymCC.TermType.isOptionType : TermType → Bool

Equations

• ty.option.isOptionType = true
• x✝.isOptionType = false

@[inline]

def Cedar.SymCC.TermType.isOptionEntityType : TermType → Bool

Equations

• (Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.entity ety)).option.isOptionEntityType = true
• x✝.isOptionEntityType = false

def Cedar.SymCC.TermType.ofType (ty : Validation.CedarType) : TermType

Equations

• Cedar.SymCC.TermType.ofType (Cedar.Validation.CedarType.bool bty) = Cedar.SymCC.TermType.prim Cedar.SymCC.TermPrimType.bool
• Cedar.SymCC.TermType.ofType Cedar.Validation.CedarType.int = Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.bitvec 64)
• Cedar.SymCC.TermType.ofType Cedar.Validation.CedarType.string = Cedar.SymCC.TermType.prim Cedar.SymCC.TermPrimType.string
• Cedar.SymCC.TermType.ofType (Cedar.Validation.CedarType.entity ety) = Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.entity ety)
• Cedar.SymCC.TermType.ofType (Cedar.Validation.CedarType.ext xty) = Cedar.SymCC.TermType.prim (Cedar.SymCC.TermPrimType.ext xty)
• Cedar.SymCC.TermType.ofType ty_2.set = (Cedar.SymCC.TermType.ofType ty_2).set
• Cedar.SymCC.TermType.ofType (Cedar.Validation.CedarType.record (Cedar.Data.Map.mk rty)) = Cedar.SymCC.TermType.record (Cedar.Data.Map.mk (Cedar.SymCC.TermType.ofRecordType rty))

def Cedar.SymCC.TermType.ofRecordType : List (Spec.Attr × Validation.QualifiedType) → List (Spec.Attr × TermType)

Equations

• Cedar.SymCC.TermType.ofRecordType [] = []
• Cedar.SymCC.TermType.ofRecordType ((a, qty) :: rty) = (a, Cedar.SymCC.TermType.ofQualifiedType qty) :: Cedar.SymCC.TermType.ofRecordType rty

def Cedar.SymCC.TermType.ofQualifiedType : Validation.QualifiedType → TermType

Equations

• Cedar.SymCC.TermType.ofQualifiedType (Cedar.Validation.Qualified.optional ty) = (Cedar.SymCC.TermType.ofType ty).option
• Cedar.SymCC.TermType.ofQualifiedType (Cedar.Validation.Qualified.required ty) = Cedar.SymCC.TermType.ofType ty

def Cedar.SymCC.instReprTermPrimType.repr : TermPrimType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Cedar.SymCC.instReprTermPrimType : Repr TermPrimType

Equations

• Cedar.SymCC.instReprTermPrimType = { reprPrec := Cedar.SymCC.instReprTermPrimType.repr }

def Cedar.SymCC.instInhabitedTermPrimType.default : TermPrimType

Equations

• Cedar.SymCC.instInhabitedTermPrimType.default = Cedar.SymCC.TermPrimType.bool

instance Cedar.SymCC.instInhabitedTermPrimType : Inhabited TermPrimType

Equations

• Cedar.SymCC.instInhabitedTermPrimType = { default := Cedar.SymCC.instInhabitedTermPrimType.default }

instance Cedar.SymCC.instDecidableEqTermPrimType : DecidableEq TermPrimType

Equations

• Cedar.SymCC.instDecidableEqTermPrimType = Cedar.SymCC.instDecidableEqTermPrimType.decEq

def Cedar.SymCC.instDecidableEqTermPrimType.decEq (x✝ x✝¹ : TermPrimType) : Decidable (x✝ = x✝¹)

Equations

• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.bool Cedar.SymCC.TermPrimType.bool = isTrue ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.bool (Cedar.SymCC.TermPrimType.bitvec n) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.bool Cedar.SymCC.TermPrimType.string = isFalse Cedar.SymCC.instDecidableEqTermPrimType.decEq._proof_2✝
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.bool (Cedar.SymCC.TermPrimType.entity ety) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.bool (Cedar.SymCC.TermPrimType.ext xty) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.bitvec n) Cedar.SymCC.TermPrimType.bool = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.bitvec a) (Cedar.SymCC.TermPrimType.bitvec b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.bitvec n) Cedar.SymCC.TermPrimType.string = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.bitvec n) (Cedar.SymCC.TermPrimType.entity ety) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.bitvec n) (Cedar.SymCC.TermPrimType.ext xty) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.string Cedar.SymCC.TermPrimType.bool = isFalse Cedar.SymCC.instDecidableEqTermPrimType.decEq._proof_11✝
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.string (Cedar.SymCC.TermPrimType.bitvec n) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.string Cedar.SymCC.TermPrimType.string = isTrue ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.string (Cedar.SymCC.TermPrimType.entity ety) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq Cedar.SymCC.TermPrimType.string (Cedar.SymCC.TermPrimType.ext xty) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.entity ety) Cedar.SymCC.TermPrimType.bool = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.entity ety) (Cedar.SymCC.TermPrimType.bitvec n) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.entity ety) Cedar.SymCC.TermPrimType.string = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.entity a) (Cedar.SymCC.TermPrimType.entity b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.entity ety) (Cedar.SymCC.TermPrimType.ext xty) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.ext xty) Cedar.SymCC.TermPrimType.bool = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.ext xty) (Cedar.SymCC.TermPrimType.bitvec n) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.ext xty) Cedar.SymCC.TermPrimType.string = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.ext xty) (Cedar.SymCC.TermPrimType.entity ety) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrimType.decEq (Cedar.SymCC.TermPrimType.ext a) (Cedar.SymCC.TermPrimType.ext b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

partial def Cedar.SymCC.instReprTermType.repr : TermType → Nat → Std.Format

instance Cedar.SymCC.instReprTermType : Repr TermType

Equations

• Cedar.SymCC.instReprTermType = { reprPrec := Cedar.SymCC.instReprTermType.repr }

def Cedar.SymCC.instInhabitedTermType.default : TermType

Equations

• Cedar.SymCC.instInhabitedTermType.default = Cedar.SymCC.TermType.prim default

instance Cedar.SymCC.instInhabitedTermType : Inhabited TermType

Equations

• Cedar.SymCC.instInhabitedTermType = { default := Cedar.SymCC.instInhabitedTermType.default }

def Cedar.SymCC.TermType.hasDecEq (ty₁ ty₂ : TermType) : Decidable (ty₁ = ty₂)

Equations

• One or more equations did not get rendered due to their size.

instance Cedar.SymCC.instDecidableEqTermType : DecidableEq TermType

Equations

• Cedar.SymCC.instDecidableEqTermType = Cedar.SymCC.TermType.hasDecEq

def Cedar.SymCC.TermPrimType.mkName : TermPrimType → String

Equations

• Cedar.SymCC.TermPrimType.bool.mkName = "bool"
• (Cedar.SymCC.TermPrimType.bitvec a).mkName = "bitvec"
• Cedar.SymCC.TermPrimType.string.mkName = "string"
• (Cedar.SymCC.TermPrimType.entity a).mkName = "entity"
• (Cedar.SymCC.TermPrimType.ext a).mkName = "ext"

def Cedar.SymCC.TermType.mkName : TermType → String

Equations

• (Cedar.SymCC.TermType.prim a).mkName = "prim"
• a.option.mkName = "option"
• a.set.mkName = "set"
• (Cedar.SymCC.TermType.record a).mkName = "record"

def Cedar.Validation.ExtType.lt : ExtType → ExtType → Bool

Equations

• Cedar.Validation.ExtType.decimal.lt Cedar.Validation.ExtType.ipAddr = true
• Cedar.Validation.ExtType.decimal.lt Cedar.Validation.ExtType.datetime = true
• Cedar.Validation.ExtType.decimal.lt Cedar.Validation.ExtType.duration = true
• Cedar.Validation.ExtType.ipAddr.lt Cedar.Validation.ExtType.datetime = true
• Cedar.Validation.ExtType.ipAddr.lt Cedar.Validation.ExtType.duration = true
• Cedar.Validation.ExtType.datetime.lt Cedar.Validation.ExtType.duration = true
• x✝¹.lt x✝ = false

instance Cedar.Validation.instLTExtType : LT ExtType

Equations

• Cedar.Validation.instLTExtType = { lt := fun (x y : Cedar.Validation.ExtType) => x.lt y = true }

instance Cedar.Validation.ExtType.decLt (x y : ExtType) : Decidable (x < y)

Equations

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

def Cedar.SymCC.TermPrimType.lt : TermPrimType → TermPrimType → Bool

Equations

• (Cedar.SymCC.TermPrimType.bitvec n₁).lt (Cedar.SymCC.TermPrimType.bitvec n₂) = decide (n₁ < n₂)
• (Cedar.SymCC.TermPrimType.entity ety₁).lt (Cedar.SymCC.TermPrimType.entity ety₂) = decide (ety₁ < ety₂)
• (Cedar.SymCC.TermPrimType.ext xty₁).lt (Cedar.SymCC.TermPrimType.ext xty₂) = decide (xty₁ < xty₂)
• x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

instance Cedar.SymCC.instLTTermPrimType : LT TermPrimType

Equations

• Cedar.SymCC.instLTTermPrimType = { lt := fun (x y : Cedar.SymCC.TermPrimType) => x.lt y = true }

instance Cedar.SymCC.TermPrimType.decLt (x y : TermPrimType) : Decidable (x < y)

Equations

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

@[irreducible]

def Cedar.SymCC.TermType.lt : TermType → TermType → Bool

Equations

• (Cedar.SymCC.TermType.prim pty₁).lt (Cedar.SymCC.TermType.prim pty₂) = decide (pty₁ < pty₂)
• ty₁.option.lt ty₂.option = ty₁.lt ty₂
• ty₁.set.lt ty₂.set = ty₁.lt ty₂
• (Cedar.SymCC.TermType.record (Cedar.Data.Map.mk rty₁)).lt (Cedar.SymCC.TermType.record (Cedar.Data.Map.mk rty₂)) = Cedar.SymCC.TermType.ltListProd✝ rty₁ rty₂
• x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

instance Cedar.SymCC.instLTTermType : LT TermType

Equations

• Cedar.SymCC.instLTTermType = { lt := fun (x y : Cedar.SymCC.TermType) => x.lt y = true }

instance Cedar.SymCC.TermType.decLt (x y : TermType) : Decidable (x < y)

Equations

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