Lean 4

Lean 4 is a dependently-typed programming language and theorem prover inheriting from Haskell, Rocq, and OCaml supporting both functional and imperative styles while remaining free of side-effects.

Quirks

Pattern synonyms

Atypical for programming languages, expressions satisfying certain properties function as patterns.

For a expression to be matchable, it must be constructed only of variables, literals, and applications of constructors. This is not unique to Lean. However, Lean allows functions to be marked as safe to reduce in a pattern context. As long as the definition reduces to a valid pattern, it'll work.https://proofassistants.stackexchange.com/questions/2438/why-can-addition-be-used-in-pattern-matching-nats-but-not-multiplication

inductive MyNat
| zero : MyNat
| succ : MyNat -> MyNat

-- Either this, attached to the decl:
@[match_pattern]
def MyNat.add : MyNat -> MyNat -> MyNat
| m, MyNat.zero => m
| m, MyNat.succ n => MyNat.succ (MyNat.add m n)

-- Or as a standalone declaration.
attribute [match_pattern] MyNat.add

Useful links