()
| 4008 | all: muts_all, |
| 4009 | aux_layout: None, |
| 4010 | }), |
| 4011 | ), |
| 4012 | ); |
| 4013 | } |
| 4014 | |
| 4015 | // Regenerate auxiliary constants for alpha-collapsed inductive blocks. |
| 4016 | // Only runs when `aux` is true (i.e., not from compile_const_no_aux which |
| 4017 | // compiles original Lean forms for metadata). |
| 4018 | if aux { |
| 4019 | let class_names: Vec<Vec<Name>> = sorted_classes |
| 4020 | .iter() |
| 4021 | .map(|class| class.iter().map(|c| c.name()).collect()) |
| 4022 | .collect(); |
| 4023 | let aux_layout_stored = mutual::generate_and_compile_aux_recursors( |
| 4024 | &cs, |
| 4025 | &class_names, |
| 4026 | lean_env, |
| 4027 | stt, |
| 4028 | kctx, |
| 4029 | )?; |
nothing calls this directly
no test coverage detected