Documentation

Cedar.Thm.SymCC.Decoder

Some facts about default*

source
@[irreducible]
theorem Cedar.Thm.default_lit_wf {εs : SymCC.SymEntities} {eidOf : Spec.EntityType → String} {ty : SymCC.TermType} (hwf_ty : SymCC.TermType.WellFormed εs ty) (hwf_eidOf : ∀ (ety : Spec.EntityType), εs.isValidEntityType ety = true → εs.isValidEntityUID { ty := ety, eid := eidOf ety } = true) :
SymCC.Term.WellFormed εs (SymCC.Decoder.defaultLit eidOf ty)

Decoder.defaultLit is well-formed if given sufficiently well-formed eidOf and ty.

source
@[irreducible]
theorem Cedar.Thm.default_lit_is_lit {eidOf : Spec.EntityType → String} {ty : SymCC.TermType} :
(SymCC.Decoder.defaultLit eidOf ty).isLiteral = true
source
@[irreducible]
theorem Cedar.Thm.default_lit_well_typed {eidOf : Spec.EntityType → String} {ty : SymCC.TermType} :
(SymCC.Decoder.defaultLit eidOf ty).typeOf = ty