(
&mut self,
members: &[KId<M>],
)
| 298 | } |
| 299 | |
| 300 | fn classify_block( |
| 301 | &mut self, |
| 302 | members: &[KId<M>], |
| 303 | ) -> Result<CheckBlockKind, TcError<M>> { |
| 304 | if members.is_empty() { |
| 305 | return Err(TcError::Other("empty check block".into())); |
| 306 | } |
| 307 | |
| 308 | let mut saw_defn = false; |
| 309 | let mut saw_recr = false; |
| 310 | let mut saw_inductive_like = false; |
| 311 | for member in members { |
| 312 | match self.get_const(member)? { |
| 313 | KConst::Defn { .. } => saw_defn = true, |
| 314 | KConst::Recr { .. } => saw_recr = true, |
| 315 | KConst::Indc { .. } | KConst::Ctor { .. } => { |
| 316 | saw_inductive_like = true; |
| 317 | }, |
| 318 | KConst::Axio { .. } | KConst::Quot { .. } => { |
| 319 | return Err(TcError::Other(format!( |
| 320 | "unsupported check block {member}: axiom/quotient member" |
| 321 | ))); |
| 322 | }, |
| 323 | } |
| 324 | } |
| 325 | |
| 326 | match (saw_defn, saw_inductive_like, saw_recr) { |
| 327 | (true, false, false) => Ok(CheckBlockKind::Defn), |
| 328 | (false, true, false) => Ok(CheckBlockKind::Inductive), |
| 329 | (false, false, true) => Ok(CheckBlockKind::Recursor), |
| 330 | _ => Err(TcError::Other( |
| 331 | "unsupported mixed check block: expected only definitions, only inductives/constructors, or only recursors" |
| 332 | .into(), |
| 333 | )), |
| 334 | } |
| 335 | } |
| 336 | |
| 337 | fn check_block_body( |
| 338 | &mut self, |
no test coverage detected