Lean.Server.Rpc.Deriving

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

Equations

Lean.Server.RpcEncodable.isOptField n = n.toString.endsWith "?"

Instances For

instance Lean.Server.RpcEncodable.instCoeTSyntaxConsSyntaxNodeKindStrNumAnonymousOfNatNatNilMkStr4 :

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

Equations

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