aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/core_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 12:58:35 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 12:58:35 -0400
commit0fa422bfaf3931aacff958cb73d44ebfa4191f4a (patch)
tree23055572341487865f0ef6cff685404f796a2410 /src/core_env.sml
parent833f4d2e0474ec3ff772107b52711289c4b648cf (diff)
Fix nasty de Bruijn substitution bug; TcSum demo
Diffstat (limited to 'src/core_env.sml')
-rw-r--r--src/core_env.sml14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/core_env.sml b/src/core_env.sml
index a4b48b8d..b399f62f 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -82,13 +82,13 @@ val liftConInExp =
val subConInExp =
U.Exp.mapB {kind = fn k => k,
con = fn (xn, rep) => fn c =>
- case c of
- CRel xn' =>
- (case Int.compare (xn', xn) of
- EQUAL => #1 rep
- | GREATER => CRel (xn' - 1)
- | LESS => c)
- | _ => c,
+ case c of
+ CRel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 rep
+ | GREATER => CRel (xn' - 1)
+ | LESS => c)
+ | _ => c,
exp = fn _ => fn e => e,
bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
| (ctx, _) => ctx}