def
Lean.Server.RpcEncoding.foldWithConstructors
{n : Type → Type u_1}
[inst : Monad n]
[inst : MonadControlT Lean.MetaM n]
[inst : MonadLiftT Lean.MetaM n]
{α : Type}
(indVal : Lean.InductiveVal)
(params : Array Lean.Expr)
(k : α → Lean.Name → Array Lean.Expr → Lean.Expr → n α)
(init : α)
:
n α
Fold over the constructors of indVal using k. Every iteration is executed in an updated
local context containing free variables for the arguments of the constructor. k is given the
ctor name, arguments, and output type. params is expected to contain free or meta variables
for the parameters of indVal.
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Server.RpcEncoding.withFieldsAux
{n : Type → Type u_1}
[inst : Monad n]
[inst : MonadControlT Lean.MetaM n]
[inst : MonadLiftT Lean.MetaM n]
{α : Type}
(indVal : Lean.InductiveVal)
(params : Array Lean.Expr)
(k : Array (Lean.Name × Lean.Expr) → n α)
(fieldNames : Unit → Array Lean.Name)
:
n α
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Server.RpcEncoding.withFields
{n : Type → Type u_1}
[inst : Monad n]
[inst : MonadControlT Lean.MetaM n]
[inst : MonadLiftT Lean.MetaM n]
{α : Type}
(indVal : Lean.InductiveVal)
(params : Array Lean.Expr)
(k : Array (Lean.Name × Lean.Expr) → n α)
:
n α
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Server.RpcEncoding.withFieldsFlattened
{n : Type → Type u_1}
[inst : Monad n]
[inst : MonadControlT Lean.MetaM n]
[inst : MonadLiftT Lean.MetaM n]
{α : Type}
(indVal : Lean.InductiveVal)
(params : Array Lean.Expr)
(k : Array (Lean.Name × Lean.Expr) → n α)
(includeSubobjectFields : optParam Bool true)
:
n α
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- One or more equations did not get rendered due to their size.