Zulip Chat Archive

Stream: general

Topic: beta reduction?

Scott Morrison (Mar 06 2019 at 05:41):

I have an expr something like (λ {k m n : ℕ} (h : k ∣ n), (nat.dvd_add_iff_left h).mpr) h₁ h₂. How do I do the beta reduction to get to (nat.dvd_add_iff_left h₁).mpr h₂?

Scott Morrison (Mar 06 2019 at 05:42):

I tried

(s, u) ← mk_simp_set ff [] [],
g ← (s.dsimplify [] g) <|> pure g

but the dsimplify fails.

Scott Morrison (Mar 06 2019 at 05:43):

g ← head_beta g

Scott Morrison (Mar 06 2019 at 05:43):

Sorry for the noise. :-)

Last updated: Dec 20 2023 at 11:08 UTC