tests/lean/1240.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            import Lean.Elab.Frontend


            open Lean Elab in

            
            #eval show IO _ from do

            
              discard <| importModules #[Import.mk Name.anonymous false] {} 0
	import Lean.Elab.Frontend

	open Lean Elab in
	#eval show IO _ from do
	discard <\| importModules #[Import.mk Name.anonymous false] {} 0