Constructs a literal expression (nat or string).
(x: Literal)
| 913 | hasher.update(&[binder_info_tag(&bi)]); |
| 914 | Expr(Arc::new(ExprData::ForallE(n, t, b, bi, hasher.finalize()))) |
| 915 | } |
| 916 | |
| 917 | /// Constructs a let-binding `let n : t := v in b`. |
| 918 | #[allow(non_snake_case)] |
| 919 | pub fn letE(n: Name, t: Expr, v: Expr, b: Expr, nd: bool) -> Self { |
| 920 | let mut hasher = blake3::Hasher::new(); |
| 921 | hasher.update(&[ELET]); |
| 922 | hasher.update(n.get_hash().as_bytes()); |
| 923 | hasher.update(t.get_hash().as_bytes()); |
| 924 | hasher.update(v.get_hash().as_bytes()); |
| 925 | hasher.update(b.get_hash().as_bytes()); |
| 926 | hasher.update(&[u8::from(nd)]); |
| 927 | Expr(Arc::new(ExprData::LetE(n, t, v, b, nd, hasher.finalize()))) |
| 928 | } |
| 929 | |
| 930 | /// Constructs a literal expression (nat or string). |
| 931 | pub fn lit(x: Literal) -> Self { |