Determine whether the recursor for this block is a large eliminator (can target any universe). Follows lean4lean's isLargeEliminator. Returns true if: 1. The inductive is NOT in Prop, OR 2. Single inductive with 0 constructors (e.g. Empty), OR 3. Single inductive with exactly 1 constructor where all non-param fields either live in Prop or appear in the return type args.
(
&mut self,
result_level: &KUniv<M>,
ind_infos: &[(KId<M>, u64, u64, Vec<KId<M>>, KExpr<M>, bool)],
)
| 2127 | ))); |
| 2128 | } |
| 2129 | } |
| 2130 | for index in &args[n_params..] { |
| 2131 | if expr_mentions_any_addr(index, root_addrs) { |
| 2132 | return Err(TcError::Other( |
| 2133 | "positivity: recursive occurrence index mentions an active inductive" |
| 2134 | .into(), |
| 2135 | )); |
| 2136 | } |
| 2137 | } |
| 2138 | Ok(()) |
| 2139 | } |
| 2140 | |
| 2141 | /// Whether an application has the exact universe/parameter specialization |
| 2142 | /// represented by one nested-family group. Multiple groups may share an |
| 2143 | /// inductive address: nested flattening keys auxiliaries by |
| 2144 | /// `(inductive, specialization)`, not by inductive address alone. |
| 2145 | fn positivity_group_matches( |
| 2146 | group: &PositivityGroup<M>, |
| 2147 | family: &Address, |
| 2148 | us: &[KUniv<M>], |
| 2149 | args: &[KExpr<M>], |
| 2150 | n_params: usize, |
| 2151 | ) -> bool { |
| 2152 | let Some(expected_universes) = group.concrete_univs.as_deref() else { |
| 2153 | return false; |
| 2154 | }; |
| 2155 | same_nested_specialization( |
| 2156 | family, |
| 2157 | expected_universes, |
| 2158 | &group.params, |
| 2159 | family, |
| 2160 | us, |
| 2161 | &args[..n_params], |
| 2162 | ) |
| 2163 | } |
| 2164 | |
| 2165 | /// Check that a field domain doesn't have block inductives in negative position. |
| 2166 | /// Follows lean4lean's `checkPositivity`: recurse through foralls, reject if |
| 2167 | /// inductive in domain (negative), accept if result is a valid inductive app |
| 2168 | /// (direct or nested). |
| 2169 | /// |
| 2170 | /// For nested inductives `J Ds is` where `J` is external and `Ds` mention block |
| 2171 | /// inductives, we recursively verify that `J`'s constructors (with `Ds` substituted |
| 2172 | /// for parameters) are strictly positive in the augmented address set. This prevents |
| 2173 | /// smuggling negative occurrences through an external inductive's parameter position. |
| 2174 | fn check_positivity_domain( |
| 2175 | &mut self, |
| 2176 | dom: &KExpr<M>, |
| 2177 | groups: &[PositivityGroup<M>], |
| 2178 | active_addrs: &[Address], |
| 2179 | ) -> Result<(), TcError<M>> { |
| 2180 | // Only occurrences containing the original block are relevant to this |
| 2181 | // positivity traversal. Helper families may recur elsewhere at unrelated |
| 2182 | // specializations (for example `Option Syntax` while traversing |
| 2183 | // `Option (SnapshotTask TacticParsedSnapshot)`); their head address alone |
| 2184 | // does not make that occurrence recursive for the root declaration. |
| 2185 | let root_addrs = |
| 2186 | groups.first().map(|group| group.addrs.as_slice()).ok_or_else(|| { |
no test coverage detected