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


            
            example (h : 0 = 1) : False := by

            
              first | trace_state; fail | contradiction


            example (h : 0 = 1) : False := by

            
              first | trace "first branch"; fail | contradiction
	example (h : 0 = 1) : False := by
	first \| trace_state; fail \| contradiction

	example (h : 0 = 1) : False := by
	first \| trace "first branch"; fail \| contradiction