Zulip Chat Archive
Stream: general
Topic: beta meta
Patrick Massot (Oct 17 2018 at 19:39):
Inside the tactic monad, can I ask Lean to beta-reduce an expr?
Simon Hudon (Oct 17 2018 at 19:39):
Yes: head_beta
Patrick Massot (Oct 17 2018 at 19:43):
Thanks. It reveals my problem was somewhere else
Last updated: Dec 20 2023 at 11:08 UTC