Documentation

Lean.Server.Rpc.Deriving

def Lean.Server.RpcEncodable.isOptField (n : Lake.Name) :

Equations

Lean.Server.RpcEncodable.isOptField n = String.endsWith (Lean.Name.toString n) "?"

Instances For

instance Lean.Server.RpcEncodable.instCoeTSyntaxConsSyntaxNodeKindStrNumAnonymousOfNatNatInstOfNatNatNilMkStr4 :

Coe (Lean.TSyntax (Lean.Name.str (Lean.Name.str (Lean.Name.str (Lean.Name.str (Lean.Name.num `_private.Lean.Server.Rpc.Deriving 0) "Lean") "Server") "RpcEncodable") "matchAltTerm")) (Lean.TSyntax `Lean.Parser.Term.matchAlt)

Equations

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