aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 19:43:48 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 19:43:48 -0500
commit24b68e6d7408f50023272e765687eab777596363 (patch)
tree36109508292ec57f01529ab31699ed8837d3f0c8 /src/elab_env.sml
parentdd4d718ac9f0a9862ebef19beb568bbedcc85848 (diff)
Tree demo working (and other assorted regressions fixed)
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 46f62727..05da56db 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -542,6 +542,9 @@ fun lookupENamed (env : env) n =
NONE => raise UnboundNamed n
| SOME x => x
+fun checkENamed (env : env) n =
+ Option.isSome (IM.find (#namedE env, n))
+
fun lookupE (env : env) x =
case SM.find (#renameE env, x) of
NONE => NotBound