summaryrefslogtreecommitdiff
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
commit50e456effc2cad22d6a61e08887816096c427658 (patch)
tree36109508292ec57f01529ab31699ed8837d3f0c8 /src/elab_env.sml
parent3af6c283c504e7e85d9e127f64a5eb72abe583ee (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