Equations
- Lean.Server.RpcEncodable.isOptField n = n.toString.endsWith "?"
Instances For
instance
Lean.Server.RpcEncodable.instCoeTSyntaxConsSyntaxNodeKindStrNumAnonymousOfNatNatNilMkStr4 :
Coe (Lean.TSyntax `_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.