Documentation

Lean.Server.Rpc.Deriving

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.