diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 62f3f69..c73e791 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -112,6 +112,24 @@ structure ExprEchoResult where type: Expression deriving Lean.ToJson +-- Describe the current state of the environment +structure EnvDescribe where + deriving Lean.FromJson +structure EnvDescribeResult where + imports : Array String + modules : Array String + deriving Lean.ToJson + +-- Describe a module +structure EnvModule where + module : String + deriving Lean.FromJson +structure EnvModuleResult where + imports: Array String + constNames: Array String + extraConstNames: Array String + deriving Lean.ToJson + -- Print all symbols in environment structure EnvCatalog where deriving Lean.FromJson