(&self)
| 86 | |
| 87 | impl<M: KernelMode> ExprData<M> { |
| 88 | pub fn info(&self) -> &ExprInfo<M> { |
| 89 | match self { |
| 90 | ExprData::Var(.., i) |
| 91 | | ExprData::FVar(.., i) |
| 92 | | ExprData::Sort(.., i) |
| 93 | | ExprData::Const(.., i) |
| 94 | | ExprData::App(.., i) |
| 95 | | ExprData::Lam(.., i) |
| 96 | | ExprData::All(.., i) |
| 97 | | ExprData::Let(.., i) |
| 98 | | ExprData::Prj(.., i) |
| 99 | | ExprData::Nat(.., i) |
| 100 | | ExprData::Str(.., i) => i, |
| 101 | } |
| 102 | } |
| 103 | } |
| 104 | |
| 105 | impl<M: KernelMode> KExpr<M> { |