(i: &Int, hasher: &mut blake3::Hasher)
| 577 | InstImplicit, |
| 578 | } |
| 579 | |
| 580 | fn binder_info_tag(bi: &BinderInfo) -> u8 { |
| 581 | match bi { |
| 582 | BinderInfo::Default => 0, |
| 583 | BinderInfo::Implicit => 1, |
| 584 | BinderInfo::StrictImplicit => 2, |
| 585 | BinderInfo::InstImplicit => 3, |
| 586 | } |
| 587 | } |
| 588 | |
| 589 | #[derive(Debug, PartialEq, Eq, Clone, Hash)] |
| 590 | pub enum Int { |
| 591 | OfNat(Nat), |
| 592 | NegSucc(Nat), |
| 593 | } |
| 594 |