169cd87dbe
@nunoplopes @aqjune
I had to add a new primitive to allow you to execute a tactic from the
`main` function. The `main` function is in the `io` monad. The new
primitive has type:
```
meta constant io.run_tactic {α : Type} (a : tactic α) : io α
```
I also added a new test that shows how to use it.
The test displays all declarations that have the `nat` prefix.
cc @kha
15 lines
426 B
Text
15 lines
426 B
Text
import system.io
|
|
|
|
open tactic
|
|
|
|
meta def get_decl_names_with_prefix (p : name) : tactic (list name) :=
|
|
do env ← get_env,
|
|
return $ env.fold [] $ λ d r,
|
|
let n := d.to_name in
|
|
if p.is_prefix_of n then n :: r else r
|
|
|
|
meta def main : io unit :=
|
|
do io.put_str "Declarations with prefix 'nat'\n",
|
|
ns ← io.run_tactic (get_decl_names_with_prefix `nat),
|
|
ns.mmap' $ λ n, io.put_str_ln $ to_string n,
|
|
return ()
|