summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 12:27:08 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 12:27:08 -0400
commit32115a531d5ed6cafa25dc7d3b88c2679e5142a5 (patch)
tree17f75e04d2559dc15a0f184c1c7da266de8a5a16 /src/elab_env.sml
parentc060d15003e3435d4d4c770d8f109f756db13ef5 (diff)
Primitive type constants
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 417eab74..2308fbb6 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -193,4 +193,13 @@ fun declBinds env (d, _) =
DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
| DVal (x, n, t, _) => pushENamedAs env x n t
+val ktype = (KType, ErrorMsg.dummySpan)
+
+fun bbind env x = #1 (pushCNamed env x ktype NONE)
+
+val basis = empty
+val basis = bbind basis "int"
+val basis = bbind basis "float"
+val basis = bbind basis "string"
+
end