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


            
            open Nat

            
            example : Nat.add zero (succ n) = succ n := by

            
              unfold Nat.add

            
              trace_state

            
              sorry
	open Nat
	example : Nat.add zero (succ n) = succ n := by
	unfold Nat.add
	trace_state
	sorry