lean4-htt/tests/pkg/user_ext/UserExt/Tst1.lean
2022-02-09 12:21:11 -08:00

14 lines
185 B
Text

import UserExt.FooExt
import UserExt.BlaExt
set_option trace.myDebug true
insert_foo hello
set_option trace.myDebug false
insert_foo world
show_foo_set
insert_bla abc
show_bla_set