Method decode

crates/ffi/src/ix/data.rs:38–46

Decode Ix.Int from Lean object. Ix.Int: ofNat (tag 0, 1 field) | negSucc (tag 1, 1 field)

(&self)

  /// Decode Ix.Int from Lean object.
  /// Ix.Int: ofNat (tag 0, 1 field) | negSucc (tag 1, 1 field)
  pub fn decode(&self) -> Int {
    let ctor = self.as_ctor();
    let nat = LeanNat::to_nat(&ctor.get(0));
    match ctor.tag() {
      0 => Int::OfNat(nat),
      1 => Int::NegSucc(nat),
      _ => panic!("Invalid Ix.Int tag: {}", ctor.tag()),
    }
  }
}

impl LeanIxSubstring<LeanOwned> {