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


            
            import Lean.Elab.Term


            elab "rt" : term => Lean.throwMaxRecDepthAt .missing


            set_option trace.Elab.step true


            #check rt + 1
	import Lean.Elab.Term

	elab "rt" : term => Lean.throwMaxRecDepthAt .missing

	set_option trace.Elab.step true

	#check rt + 1