Cedar.Spec.Expr

source

inductive Cedar.Spec.Var :

Type

principal : Var
action : Var
resource : Var
context : Var

Instances For

source

inductive Cedar.Spec.UnaryOp :

Type

not : UnaryOp
neg : UnaryOp
isEmpty : UnaryOp
like (p : Pattern) : UnaryOp
is (ety : EntityType) : UnaryOp

Instances For

source

inductive Cedar.Spec.BinaryOp :

Type

eq : BinaryOp
mem : BinaryOp
hasTag : BinaryOp
getTag : BinaryOp
less : BinaryOp
lessEq : BinaryOp
add : BinaryOp
sub : BinaryOp
mul : BinaryOp
contains : BinaryOp
containsAll : BinaryOp
containsAny : BinaryOp

Instances For

source

inductive Cedar.Spec.Expr :

Type

lit (p : Prim) : Expr
var (v : Var) : Expr
ite (cond thenExpr elseExpr : Expr) : Expr
and (a b : Expr) : Expr
or (a b : Expr) : Expr
unaryApp (op : UnaryOp) (expr : Expr) : Expr
binaryApp (op : BinaryOp) (a b : Expr) : Expr
getAttr (expr : Expr) (attr : Attr) : Expr
hasAttr (expr : Expr) (attr : Attr) : Expr
set (ls : List Expr) : Expr
record (map : List (Attr × Expr)) : Expr
call (xfn : ExtFun) (args : List Expr) : Expr

Instances For

source

instance Cedar.Spec.instReprVar :

Repr Var

Equations

Cedar.Spec.instReprVar = { reprPrec := Cedar.Spec.instReprVar.repr }

source

def Cedar.Spec.instReprVar.repr :

Var → Nat → Std.Format

Equations

Cedar.Spec.instReprVar.repr Cedar.Spec.Var.principal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Var.principal")).group prec✝
Cedar.Spec.instReprVar.repr Cedar.Spec.Var.action prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Var.action")).group prec✝
Cedar.Spec.instReprVar.repr Cedar.Spec.Var.resource prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Var.resource")).group prec✝
Cedar.Spec.instReprVar.repr Cedar.Spec.Var.context prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Var.context")).group prec✝

Instances For

source

instance Cedar.Spec.instDecidableEqVar :

DecidableEq Var

Equations

Cedar.Spec.instDecidableEqVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Cedar.Spec.instInhabitedVar :

Inhabited Var

Equations

Cedar.Spec.instInhabitedVar = { default := Cedar.Spec.instInhabitedVar.default }

source

def Cedar.Spec.instInhabitedVar.default :

Var

Equations

Cedar.Spec.instInhabitedVar.default = Cedar.Spec.Var.principal

Instances For

source

def Cedar.Spec.instReprUnaryOp.repr :

UnaryOp → Nat → Std.Format

Equations

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

Instances For

source

instance Cedar.Spec.instReprUnaryOp :

Repr UnaryOp

Equations

Cedar.Spec.instReprUnaryOp = { reprPrec := Cedar.Spec.instReprUnaryOp.repr }

source

def Cedar.Spec.instDecidableEqUnaryOp.decEq (x✝ x✝¹ : UnaryOp) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

instance Cedar.Spec.instDecidableEqUnaryOp :

DecidableEq UnaryOp

Equations

Cedar.Spec.instDecidableEqUnaryOp = Cedar.Spec.instDecidableEqUnaryOp.decEq

source

def Cedar.Spec.instInhabitedUnaryOp.default :

UnaryOp

Equations

Cedar.Spec.instInhabitedUnaryOp.default = Cedar.Spec.UnaryOp.not

Instances For

source

instance Cedar.Spec.instInhabitedUnaryOp :

Inhabited UnaryOp

Equations

Cedar.Spec.instInhabitedUnaryOp = { default := Cedar.Spec.instInhabitedUnaryOp.default }

source

def Cedar.Spec.instReprBinaryOp.repr :

BinaryOp → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.eq")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.mem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.mem")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.hasTag prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.hasTag")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.getTag prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.getTag")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.less prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.less")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.lessEq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.lessEq")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.add prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.add")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.sub")).group prec✝
Cedar.Spec.instReprBinaryOp.repr Cedar.Spec.BinaryOp.mul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.BinaryOp.mul")).group prec✝

Instances For

source

instance Cedar.Spec.instReprBinaryOp :

Repr BinaryOp

Equations

Cedar.Spec.instReprBinaryOp = { reprPrec := Cedar.Spec.instReprBinaryOp.repr }

source

instance Cedar.Spec.instDecidableEqBinaryOp :

DecidableEq BinaryOp

Equations

Cedar.Spec.instDecidableEqBinaryOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Cedar.Spec.instInhabitedBinaryOp.default :

BinaryOp

Equations

Cedar.Spec.instInhabitedBinaryOp.default = Cedar.Spec.BinaryOp.eq

Instances For

source

instance Cedar.Spec.instInhabitedBinaryOp :

Inhabited BinaryOp

Equations

Cedar.Spec.instInhabitedBinaryOp = { default := Cedar.Spec.instInhabitedBinaryOp.default }

source

partial def Cedar.Spec.instReprExpr.repr :

Expr → Nat → Std.Format

source

instance Cedar.Spec.instReprExpr :

Repr Expr

Equations

Cedar.Spec.instReprExpr = { reprPrec := Cedar.Spec.instReprExpr.repr }

source

instance Cedar.Spec.instInhabitedExpr :

Inhabited Expr

Equations

Cedar.Spec.instInhabitedExpr = { default := Cedar.Spec.instInhabitedExpr.default }

source

def Cedar.Spec.instInhabitedExpr.default :

Expr

Equations

Cedar.Spec.instInhabitedExpr.default = Cedar.Spec.Expr.lit default

Instances For

source

def Cedar.Spec.decExpr (x y : Expr) :

Decidable (x = y)

Equations

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

Instances For

source

instance Cedar.Spec.instDecidableEqExpr :

DecidableEq Expr

Equations

Cedar.Spec.instDecidableEqExpr = Cedar.Spec.decExpr