Extract the value expression from a ConstantInfo, if it has one.
(ci: &LeanConstantInfo)
| 2373 | num_params: Nat::from(indc.n_params as u64), |
| 2374 | num_indices: Nat::from(indc.n_indices as u64), |
| 2375 | all: all_below_names.to_vec(), |
| 2376 | ctors: ctor_names, |
| 2377 | num_nested: Nat::from(0u64), |
| 2378 | is_rec: true, |
| 2379 | // Reflexivity is inherited from the parent (see `build_below_indc`). |
| 2380 | // The `ConstantInfo::InductInfo` hash includes `is_reflexive`, so the |
| 2381 | // regenerated `.below` must carry the same flag as Lean's original. |
| 2382 | is_reflexive: indc.is_reflexive, |
| 2383 | is_unsafe: indc.is_unsafe, |
| 2384 | }; |
| 2385 | let ctors: Vec<ConstructorVal> = indc |
no outgoing calls
no test coverage detected