Cedar.Spec.Json

This file derives Lean.ToJson for the specification types that DRT and the FFI serialize. The instances live here, rather than beside the types, so that a program that uses Cedar.Spec without this module doesn't link the Lean package.

source

def Cedar.Data.instToJsonSet.toJson {α✝ : Type u_1} [Lean.ToJson α✝] :

Set α✝ → Lean.Json

Equations

Cedar.Data.instToJsonSet.toJson (Cedar.Data.Set.mk a) = Lean.Json.mkObj [("mk", Lean.Json.mkObj [("l", Lean.toJson a)])]

Instances For

source

@[instance_reducible]

instance Cedar.Data.instToJsonSet {α✝ : Type u_1} [Lean.ToJson α✝] :

Lean.ToJson (Set α✝)

Equations

Cedar.Data.instToJsonSet = { toJson := Cedar.Data.instToJsonSet.toJson }

source

def Cedar.Spec.instToJsonName.toJson :

Name → Lean.Json

Equations

Cedar.Spec.instToJsonName.toJson x✝ = Lean.Json.mkObj [[("id", Lean.toJson x✝.id)], [("path", Lean.toJson x✝.path)]].flatten

Instances For

source

@[instance_reducible]

instance Cedar.Spec.instToJsonName :

Lean.ToJson Name

Equations

Cedar.Spec.instToJsonName = { toJson := Cedar.Spec.instToJsonName.toJson }

source

def Cedar.Spec.instToJsonEntityUID.toJson :

EntityUID → Lean.Json

Equations

Cedar.Spec.instToJsonEntityUID.toJson x✝ = Lean.Json.mkObj [[("ty", Lean.toJson x✝.ty)], [("eid", Lean.toJson x✝.eid)]].flatten

Instances For

source

@[instance_reducible]

instance Cedar.Spec.instToJsonEntityUID :

Lean.ToJson EntityUID

Equations

Cedar.Spec.instToJsonEntityUID = { toJson := Cedar.Spec.instToJsonEntityUID.toJson }

source

@[instance_reducible]

instance Cedar.Spec.instToJsonPolicyID :

Lean.ToJson PolicyID

Equations

Cedar.Spec.instToJsonPolicyID = { toJson := fun (s : String) => Lean.Json.str s }

source

def Cedar.Spec.instToJsonDecision.toJson :

Decision → Lean.Json

Equations

Instances For

source

@[instance_reducible]

instance Cedar.Spec.instToJsonDecision :

Lean.ToJson Decision

Equations

Cedar.Spec.instToJsonDecision = { toJson := Cedar.Spec.instToJsonDecision.toJson }

source

def Cedar.Spec.instToJsonResponse.toJson :

Response → Lean.Json

Equations

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

Instances For

source

@[instance_reducible]

instance Cedar.Spec.instToJsonResponse :

Lean.ToJson Response

Equations

Cedar.Spec.instToJsonResponse = { toJson := Cedar.Spec.instToJsonResponse.toJson }