Lean3 match multiple constructors

Stream: new members

[Kunwar Shaanjeet Singh Grover]

Hi! I'm just trying to understand lean syntax using an example:

structure var :=
mk :: (idx : ℕ)

inductive Expr
| atom : var -> Expr
| not  : Expr -> Expr
| and  : Expr -> Expr -> Expr
| or   : Expr -> Expr -> Expr
| impl : Expr -> Expr -> Expr

def size : Expr → nat
| (atom v) := 1
| (Expr.not e) := (size e) + 1
| (Expr.and e1 e2) := (size e1) + (size e2) + 1
| (Expr.or e1 e2) := (size e1) + (size e2) + 1
| (Expr.impl e1 e2) := (size e1) + (size e2) + 1

Is there any way to match multiple Expr constructors? Something like:

structure var :=
mk :: (idx : ℕ)

inductive Expr
| atom : var -> Expr
| not  : Expr -> Expr
| and  : Expr -> Expr -> Expr
| or   : Expr -> Expr -> Expr
| impl : Expr -> Expr -> Expr

def size : Expr → nat
| (atom v) := 1
| (Expr.not e) := (size e) + 1
| (Expr e1 e2) := (size e1) + (size e2) + 1 -- Match all remaining constructors?

[Kunwar Shaanjeet Singh Grover]

Disclaimer: The question is from a homework exercise. But the homework is to implement the size function which I have already done. I'm only looking at better syntactic ways to implement it :)

[Daniel Fabian]

you can use _ as a wild card. I.e. _ at the end should do it.

[Kunwar Shaanjeet Singh Grover]

How do I extract e1 and e2 out of _ though?

[Yaël Dillies]

Ah to do that you can't I'm afraid.

[Kunwar Shaanjeet Singh Grover]

sad :(. Thanks anyway!

[Kyle Miller]

@Kunwar Shaanjeet Singh Grover If you expect to do other types of folds on Expr, then one thing you can do is define a generic fold function that takes functions for the three possible arities of constructors:

namespace Expr

def fold {α : Type*} (f : var → α) (g : α → α) (h : α → α → α) : Expr → α
| (atom v) := f v
| (not e) := g (fold e)
| (and e1 e2) := h (fold e1) (fold e2)
| (or e1 e2) := h (fold e1) (fold e2)
| (impl e1 e2) := h (fold e1) (fold e2)

end Expr

def size (e : Expr) : nat := e.fold (λ _, 1) (+1) (+)

def atoms (e : Expr) : set var := e.fold (λ v, {v}) id (∪)