fix(tomograph): Import search directory

This commit is contained in:
Leni Aniva 2025-07-02 15:13:43 -07:00
parent 80fb7f30c3
commit 48046b8b5a
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 5 additions and 0 deletions

View File

@ -1,5 +1,6 @@
/- A tool for analysing Lean source code. -/
import Pantograph.Frontend
import Pantograph.Library
open Lean
@ -18,6 +19,8 @@ def dissect (args: List String): IO UInt32 := do
IO.println s!"🐈 {step.stx.getKind.toString}"
for (tree, i) in step.trees.zipIdx do
IO.println s!"🌲[{i}] {← tree.toString}"
for (msg, i) in step.msgs.zipIdx do
IO.println s!"🔈[{i}] {← msg.toString}"
let (_, _) ← frontendM.run context |>.run state
return 0
@ -31,6 +34,8 @@ def help : IO UInt32 := do
def main (args : List String) : IO UInt32 := do
let command :: args := args | help
unsafe do
Pantograph.initSearch ""
match command with
| "dissect" => dissect args
| _ => fail s!"Unknown command {command}"