diff options
author | Nadrieril | 2020-01-29 21:35:28 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-29 21:35:28 +0000 |
commit | 280b3174476ef8fe5a98f3614f4fe253fa243d8c (patch) | |
tree | 93062b08134200b703670b0fe91898a437a924d2 /dhall/src/semantics/phase | |
parent | 22bec94618454f57773716870f5624579ab712ce (diff) |
Finally get rid of all of the shift/subst_shift !
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d40456b..fa80b6e 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -638,15 +638,13 @@ pub(crate) fn normalize_one_layer( ), // Those cases have already been completely handled in the typechecking phase (using // `RetWhole`), so they won't appear here. - ExprKind::Lam(_, _, _) - | ExprKind::Pi(_, _, _) + ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) | ExprKind::Embed(_) | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } - ExprKind::Let(_, _, val, body) => { - Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) - } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), |