Unfolding expr

Stream: general

[Tomas Skrivan]

What are the available functions to unfold definitions inside of an expression? Currently I'm using tactic.whnf but sometimes it unfolds too much. An example:

def uncurry {X Y Z : Type} (f : X → Y → Z) (xy : X×Y) := f xy.1 xy.2

def swap {X Y : Type} := uncurry $ λ (x : X) (y : Y), (y, x)

-- Case 1: uncurry does not get unfolded
run_cmd do
  tactic.to_expr ``(@swap) >>= tactic.whnf >>= tactic.trace
-- λ {X Y : Type}, uncurry (λ (x : X) (y : Y), (y, x))

-- Case 2: uncurry gets unfolded
run_cmd do
  tactic.to_expr ``(@swap ℕ ℤ) >>= tactic.whnf >>= tactic.trace
-- λ (xy : ℕ × ℤ), (λ (x : ℕ) (y : ℤ), (y, x)) xy.fst xy.snd

In the second case, I would like to unfold only swap i.e. probably some kind of variant of tactic.whnf that does not unfold recursively.

[Mario Carneiro]

does dunfold swap do what you want?

[Kevin Buzzard]

There's also delta swap

[Tomas Skrivan]

Thank! tactic.delta did the trick for me. I do not know the name of the constant to unfold every time, so I have definedhead_delta

meta def head_delta : expr → tactic expr
| (expr.const name lvl) :=
  tactic.delta [name] (expr.const name lvl)
| (expr.app f x) := do
  f ← head_delta f,
  pure (expr.app f x)
| e := tactic.fail ("Failed to expand head of " ++ to_string e)

And this works great in my use case.