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

Equations

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

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

• Lean.Server.RpcEncodable.instCoeTSyntaxConsSyntaxNodeKindStrNumAnonymousOfNatNatInstOfNatNatNilMkStr4 = { coe := fun s => { raw := s.raw } }