lean4-htt/tests/pkg/initialize/Initialize/NoModule.lean
2026-01-29 15:32:56 +00:00

9 lines
147 B
Text

import Initialize.Basic
/-- info: 42 -/
#guard_msgs in
#eval initNat
/-- info: #["ref3", "ref2", "ref1", "ref4"] -/
#guard_msgs in
#eval ref.get