matching expressions

Stream: lean4

[Arthur Paulino]

What would we need to equip ourselves with in order to be able to do things like this in Lean 4?

do t ← infer_type h,
   match t with
   | `(%%a ∨ %%b) := cases h >> case_cont s cont >> return tt
...

[Gabriel Ebner]

Answer 1: use the quote4 library:

match t with
| ~q($a ∨ $b) => ...

[Gabriel Ebner]

Answer 2: manually destruct the expression.

if t.isAppOfArity ``Or 2 then
  let a := t.getArg! 0
  let b := t.getArg! 1

[Gabriel Ebner]

Answer 3: #xy. Instead of trying to port finish, try to integrate aesop.

[Arthur Paulino]

Thanks!

[Arthur Paulino]

I asked this question because it can simplify tactic writing in mathlib4. Should we use your lib there?