Code generation of recursors #191

New Issue

aniva · 2025-04-14T16:23:38-07:00

aniva commented

2025-04-14 16:23:38 -07:00

Unless https://leanprover-community.github.io/archive/stream/270676-lean4/topic/code.20generator.20does.20not.20support.20recursor.html gets fixed, Lean will not be able to generate code for recursors. In these cases we need to manually compile them via a similar mechanism to compile_inductive.

Unless https://leanprover-community.github.io/archive/stream/270676-lean4/topic/code.20generator.20does.20not.20support.20recursor.html gets fixed, Lean will not be able to generate code for recursors. In these cases we need to manually compile them via a similar mechanism to [compile_inductive](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Util/CompileInductive.html#Mathlib.Util.%C2%ABcommandCompile_inductive%25_%C2%BB).

aniva added this to the 0.4.0 milestone 2025-04-14 16:23:38 -07:00

aniva added the

labels 2025-04-14 16:23:38 -07:00

aniva self-assigned this 2025-04-14 16:23:39 -07:00

aniva commented

2025-04-14 16:48:36 -07:00

Also vide: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.E2.9C.94.20.22code.20generator.20does.20not.20support.20recursor.22

This is related to generating recursive functions.

Also vide: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.E2.9C.94.20.22code.20generator.20does.20not.20support.20recursor.22 This is related to generating recursive functions.

Sign in to join this conversation.