feat: Read dependencies of library symbols #32
|
@ -85,6 +85,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
return .ok {
|
||||
type := ← serialize_expression state.options info.type,
|
||||
value? := ← value?.mapM (λ v => serialize_expression state.options v),
|
||||
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
|
||||
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
|
||||
module? := module?
|
||||
}
|
||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||
|
|
|
@ -113,11 +113,15 @@ structure LibInspect where
|
|||
-- If true/false, show/hide the value expressions; By default definitions
|
||||
-- values are shown and theorem values are hidden.
|
||||
value?: Option Bool := .some false
|
||||
-- If true, show the type and value dependencies
|
||||
dependency?: Option Bool := .some false
|
||||
deriving Lean.FromJson
|
||||
structure LibInspectResult where
|
||||
type: Expression
|
||||
value?: Option Expression := .none
|
||||
module?: Option String
|
||||
typeDependency?: Option (Array String) := .none
|
||||
valueDependency?: Option (Array String) := .none
|
||||
deriving Lean.ToJson
|
||||
|
||||
/-- Set options; See `Options` struct above for meanings -/
|
||||
|
|
Loading…
Reference in New Issue