Method proj

crates/common/src/env.rs:944–951

Constructs a projection expression (type name, field index, struct expr).

(n: Name, i: Nat, e: Expr)

    };
    Expr(Arc::new(ExprData::Lit(x, hasher.finalize())))
  }

  /// Constructs a metadata-annotated expression.
  pub fn mdata(xs: Vec<(Name, DataValue)>, e: Expr) -> Self {
    let mut hasher = blake3::Hasher::new();
    hasher.update(&[EMDATA]);
    hasher.update(&Nat::from(xs.len() as u64).to_le_bytes());
    for (name, dv) in &xs {
      hasher.update(name.get_hash().as_bytes());
      hash_data_value(dv, &mut hasher);
    }