Documentation

Strata.DL.SMT.Function

Based on Cedar's Term language. (https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/Cedar/SymCC/Function.lean) This file defines an ADT that represents functions over terms.

inductive Strata.SMT.Function :

uf : UF → Function

Instances For

instance Strata.SMT.instReprFunction :

Equations

Strata.SMT.instReprFunction = { reprPrec := Strata.SMT.instReprFunction.repr }

def Strata.SMT.instReprFunction.repr :

Function → Nat → Std.Format

Equations

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

Instances For

def Strata.SMT.instDecidableEqFunction.decEq (x✝ x✝¹ : Function) :

Decidable (x✝ = x✝¹)

Equations

Strata.SMT.instDecidableEqFunction.decEq (Strata.SMT.Function.uf a) (Strata.SMT.Function.uf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

instance Strata.SMT.instDecidableEqFunction :

DecidableEq Function

Equations

Strata.SMT.instDecidableEqFunction = Strata.SMT.instDecidableEqFunction.decEq

instance Strata.SMT.instInhabitedFunction :

Inhabited Function

Equations

Strata.SMT.instInhabitedFunction = { default := Strata.SMT.instInhabitedFunction.default }

def Strata.SMT.instInhabitedFunction.default :

Equations

Strata.SMT.instInhabitedFunction.default = Strata.SMT.Function.uf default

Instances For

def Strata.SMT.Function.argType (ff : Function) (i : Nat) :

Option TermType

Equations

(Strata.SMT.Function.uf a).argType i = match a.args[i]? with | none => none | some arg => some arg.ty

Instances For

def Strata.SMT.Function.outType :

Function → TermType

Equations

(Strata.SMT.Function.uf a).outType = a.out

Instances For

def Strata.SMT.Function.isUF :

Function → Bool

Equations

(Strata.SMT.Function.uf a).isUF = true

Instances For