Zulip Chat Archive

Stream: lean4

Topic: Elaboration Strategies


view this post on Zulip François G. Dorais (Jan 08 2021 at 12:28):

Closed issue #201 suggests that special elaboration strategies like Lean 3's elab_as_eliminator are no longer useful in Lean 4. What has changed?

view this post on Zulip François G. Dorais (Jan 09 2021 at 14:09):

I've been working on porting some low-level Lean 3 code which makes strong use of term mode and custom recursors. Here is a trick to work around the absence of elab_as_eliminator in case someone else is struggling with similar issues.

It looks like *.recOn and friends are always elaborated just like any other terms but in Lean 4 we can specify individual optional arguments by name. The motive in *.recOn and friends seems to always be called motive (rather than a nondescript name like C in Lean 3), so *.recOn (motive := fun _ => _) ... often works to simulate what elab_as_eliminator would do. Sometimes fun _ => _ is not enough and a bit more of the motive needs to be specified but it's generally a good starting point.

In tactic mode, it appears that the induction and cases tactics have gained some additional powers that may make elaboration strategies obsolete but I haven't explored this yet.


Last updated: May 18 2021 at 22:15 UTC