summaryrefslogtreecommitdiff
path: root/dhall/src/typecheck.rs
diff options
context:
space:
mode:
authorNadrieril2019-04-06 11:09:23 +0200
committerNadrieril2019-04-06 11:09:23 +0200
commit0cf4d3845e75ac25e35c5e73eb2dfd58c5450af6 (patch)
tree4cf5119a66fc7baeb66cb44a171d5a290429da18 /dhall/src/typecheck.rs
parent5b0e81c215fa6323635ca1bf49a86aeef0ba80f8 (diff)
Factor out shift/subst/shift dance
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs5
1 files changed, 1 insertions, 4 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 75e6e1d..145de63 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -268,10 +268,7 @@ where
let tA2 = normalized_type_with(ctx, a.clone())?;
if prop_equal(tA.as_ref(), tA2.as_ref()) {
let vx0 = &V(x.clone(), 0);
- let a2 = shift(1, vx0, a);
- let tB2 = subst(vx0, &a2, &tB);
- let tB3 = shift(-1, vx0, &tB2);
- return Ok(tB3);
+ return Ok(subst_shift(vx0, &a, &tB));
} else {
Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2)))
}