Pops the given frame. If the frame has an additional inductive step, then return it, otherwise return `None`.
(&self, induct: ClassFrame<'a>)
| 445 | /// Pops the given frame. If the frame has an additional inductive step, |
| 446 | /// then return it, otherwise return `None`. |
| 447 | fn pop_class(&self, induct: ClassFrame<'a>) -> Option<ClassFrame<'a>> { |
| 448 | match induct { |
| 449 | ClassFrame::Union { tail, .. } => { |
| 450 | if tail.is_empty() { |
| 451 | None |
| 452 | } else { |
| 453 | Some(ClassFrame::Union { |
| 454 | head: &tail[0], |
| 455 | tail: &tail[1..], |
| 456 | }) |
| 457 | } |
| 458 | } |
| 459 | ClassFrame::Binary {..} => None, |
| 460 | ClassFrame::BinaryLHS { op, rhs, .. } => { |
| 461 | Some(ClassFrame::BinaryRHS { |
| 462 | op: op, |
| 463 | rhs: rhs, |
| 464 | }) |
| 465 | } |
| 466 | ClassFrame::BinaryRHS {..} => None, |
| 467 | } |
| 468 | } |
| 469 | } |
| 470 | |
| 471 | impl<'a> Frame<'a> { |