summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 10:58:11 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commitf2ada9d9761c3aa7575571fd93629b79350a1425 (patch)
tree4dd385ff8a2fd742a48ecb1db7d385574f6a679c /src/elab_env.sml
parent8ef0d043574638a48c71b7c4c9844fc05973f13d (diff)
Trial version of completing table fields
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml7
1 files changed, 3 insertions, 4 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 34071664..f492bc94 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -940,13 +940,12 @@ fun lookupENamed (env : env) n =
NONE => raise UnboundNamed n
| SOME x => x
+(* TODO Why does this work better than using #renameE? *)
fun matchEByPrefix (env: env) (prefix: string): (string * con) list =
List.mapPartial (fn (name, value) => if String.isPrefix prefix name
- then case value of
- Rel' (_, x) => SOME (name, x)
- | Named' (_, x) => SOME (name, x)
+ then SOME (name, value)
else NONE)
- (SM.listItemsi (#renameE env))
+ (#relE env @ IM.listItems (#namedE env))
fun checkENamed (env : env) n =
Option.isSome (IM.find (#namedE env, n))