HepLean Documentation

Lean.Server.Rpc.Deriving

Equations
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.