5 lines
92 B
Text
5 lines
92 B
Text
open nat
|
|
namespace foo
|
|
open int
|
|
run_command tactic.open_namespaces >>= tactic.trace
|
|
end foo
|