Method all

crates/common/src/env.rs:891–899

Constructs a dependent function type (forall / Pi).

(n: Name, t: Expr, b: Expr, bi: BinderInfo)

    hasher.update(&[EAPP]);
    hasher.update(f.get_hash().as_bytes());
    hasher.update(a.get_hash().as_bytes());
    Expr(Arc::new(ExprData::App(f, a, hasher.finalize())))
  }

  /// Constructs a lambda abstraction `fun (n : t) => b`.
  pub fn lam(n: Name, t: Expr, b: Expr, bi: BinderInfo) -> Self {
    let mut hasher = blake3::Hasher::new();
    hasher.update(&[ELAM]);
    hasher.update(n.get_hash().as_bytes());
    hasher.update(t.get_hash().as_bytes());
    hasher.update(b.get_hash().as_bytes());
    hasher.update(&[binder_info_tag(&bi)]);