Questions tagged [addition]
The addition tag has no usage guidance.
1
question
4
votes
1
answer
87
views
Why can addition be used in pattern matching Nats but not multiplication
Here's a simple dummy function in Lean 4:
def foo : Nat → Nat
| (m*2) => m
| (m+2) => m
| (m+1) => m
| (0) => 0
Lean has no trouble ...