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


            
            /-! Partial syntax should not suppress trace output. -/


            set_option pp.rawOnError true

            
            set_option trace.Elab.command true

            
            def f
	/-! Partial syntax should not suppress trace output. -/

	set_option pp.rawOnError true
	set_option trace.Elab.command true
	def f