Constructs a bound variable expression from a de Bruijn index.
(x: Nat)
| 826 | /// Returns the precomputed Blake3 hash of this expression. |
| 827 | pub fn get_hash(&self) -> &Hash { |
| 828 | match &*self.0 { |
| 829 | ExprData::Bvar(_, h) |
| 830 | | ExprData::Fvar(_, h) |
| 831 | | ExprData::Mvar(_, h) |
| 832 | | ExprData::Sort(_, h) |
| 833 | | ExprData::Const(.., h) |
| 834 | | ExprData::App(.., h) |
| 835 | | ExprData::Lam(.., h) |
| 836 | | ExprData::ForallE(.., h) |