Function strip_mdata

crates/compile/src/congruence.rs:337–343

Strip Mdata wrappers from an expression.

(e: &Expr)

/// Strip Mdata wrappers from an expression.
pub fn strip_mdata(e: &Expr) -> &Expr {
  let mut cur = e;
  while let ExprData::Mdata(_, inner, _) = cur.as_data() {
    cur = inner;
  }
  cur
}

pub fn check_nat_eq(a: &Nat, b: &Nat, field: &str) -> Result<(), String> {
  let av = a.to_u64().unwrap_or(u64::MAX);