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


            
            import Lean.Elab.Tactic


            open Lean Elab Tactic in

            
            elab "print!" : tactic => do

            
              logInfo "foo"

            
              throwError "error"


            example : True := by

            
              print!

            
              admit
	import Lean.Elab.Tactic

	open Lean Elab Tactic in
	elab "print!" : tactic => do
	logInfo "foo"
	throwError "error"

	example : True := by
	print!
	admit