| 901 | hasher.update(b.get_hash().as_bytes()); |
| 902 | hasher.update(&[binder_info_tag(&bi)]); |
| 903 | Expr(Arc::new(ExprData::Lam(n, t, b, bi, hasher.finalize()))) |
| 904 | } |
| 905 | |
| 906 | /// Constructs a dependent function type (forall / Pi). |
| 907 | pub fn all(n: Name, t: Expr, b: Expr, bi: BinderInfo) -> Self { |
| 908 | let mut hasher = blake3::Hasher::new(); |
| 909 | hasher.update(&[EALL]); |
| 910 | hasher.update(n.get_hash().as_bytes()); |
| 911 | hasher.update(t.get_hash().as_bytes()); |
| 912 | hasher.update(b.get_hash().as_bytes()); |
| 913 | hasher.update(&[binder_info_tag(&bi)]); |
| 914 | Expr(Arc::new(ExprData::ForallE(n, t, b, bi, hasher.finalize()))) |
| 915 | } |