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


            
            unfoldReduceMatch.lean:2:0-2:7: warning: declaration uses 'sorry'

            
            n : Nat

            
            ⊢ (Nat.zero.add n).succ = n.succ
	unfoldReduceMatch.lean:2:0-2:7: warning: declaration uses 'sorry'
	n : Nat
	⊢ (Nat.zero.add n).succ = n.succ