Topic: Elaboration Strategies
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?
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