Method decode

crates/ffi/src/ix/constant.rs:54–62

Decode Ix.ConstantVal from Lean object. ConstantVal = { name : Name, levelParams : Array Name, type : Expr }

(&self)

  /// Decode Ix.ConstantVal from Lean object.
  /// ConstantVal = { name : Name, levelParams : Array Name, type : Expr }
  pub fn decode(&self) -> ConstantVal {
    let ctor = self.as_ctor();
    let name = LeanIxName(ctor.get(0)).decode();
    let level_params: Vec<Name> =
      ctor.get(1).as_array().map(|x| LeanIxName(x).decode());
    let typ = LeanIxExpr(ctor.get(2)).decode();

    ConstantVal { name, level_params, typ }
  }
}

// =============================================================================