## Stream: new members

### Topic: Lean3 match multiple constructors

#### Kunwar Shaanjeet Singh Grover (Feb 13 2022 at 12:37):

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 (Feb 13 2022 at 12:38):

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 (Feb 13 2022 at 12:39):

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

#### Kunwar Shaanjeet Singh Grover (Feb 13 2022 at 12:41):

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

#### Yaël Dillies (Feb 13 2022 at 12:52):

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

#### Kyle Miller (Feb 13 2022 at 15:40):

@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 (∪)


Last updated: Dec 20 2023 at 11:08 UTC