Constructs a free variable expression.
(x: Name)
| 834 | | ExprData::App(.., h) |
| 835 | | ExprData::Lam(.., h) |
| 836 | | ExprData::ForallE(.., h) |
| 837 | | ExprData::LetE(.., h) |
| 838 | | ExprData::Lit(_, h) |
| 839 | | ExprData::Mdata(.., h) |
| 840 | | ExprData::Proj(.., h) => h, |
| 841 | } |
| 842 | } |
| 843 | /// Constructs a bound variable expression from a de Bruijn index. |
| 844 | pub fn bvar(x: Nat) -> Self { |