Determine which batch a `.brecOn` definition belongs to. Batch 0: `.brecOn.go` (must compile first, `.brecOn` references it) Batch 1: `.brecOn` (the main definition) Batch 2: `.brecOn.eq` (proof of unfolding equation, references `.brecOn`)
(name: &Name)
| 1038 | name: c.name.clone(), |
| 1039 | level_params: bi.level_params.clone(), |
| 1040 | typ: c.typ.clone(), |
| 1041 | }, |
| 1042 | induct: bi.name.clone(), |
| 1043 | cidx: Nat::from(ci as u64), |
| 1044 | num_params: Nat::from(c.n_params as u64), |
| 1045 | num_fields: Nat::from(c.n_fields as u64), |
| 1046 | // A `.below` constructor inherits the parent inductive's safety; Lean's |
| 1047 | // kernel requires ctor safety to match the enclosing inductive. |
| 1048 | is_unsafe: bi.is_unsafe, |
| 1049 | }) |
no test coverage detected