Zulip Chat Archive

Stream: lean4

Topic: matching expressions


Arthur Paulino (Feb 09 2022 at 21:15):

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 (Feb 10 2022 at 11:12):

Answer 1: use the quote4 library:

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

Gabriel Ebner (Feb 10 2022 at 11:13):

Answer 2: manually destruct the expression.

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

Gabriel Ebner (Feb 10 2022 at 11:14):

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

Arthur Paulino (Feb 10 2022 at 12:05):

Thanks!

Arthur Paulino (Feb 10 2022 at 12:12):

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


Last updated: Dec 20 2023 at 11:08 UTC