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


            
            example : Nat → Nat := by

            
              refine' (fun x => _)

            
              trace_state

            
              sorry


            example : Nat → Nat := by

            
              refine' (fun x => ?_)

            
              trace_state

            
              sorry
	example : Nat → Nat := by
	refine' (fun x => _)
	trace_state
	sorry

	example : Nat → Nat := by
	refine' (fun x => ?_)
	trace_state
	sorry