Questions tagged [addition]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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 ...
Nate Glenn's user avatar