Mercurial > urweb

comparison src/cjr_env.sml @ 56:d3cc191cb25f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Separate compilation and automatic basis importation
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 14:23:05 -0400
parents 537db4ee89f4
children 717b6f8d8505
comparison
equal deleted inserted replaced
55:5c97b7cd912b 56:d3cc191cb25f
119 case d of 119 case d of
120 DVal (x, n, t, _) => pushENamed env x n t 120 DVal (x, n, t, _) => pushENamed env x n t
121 | DFun (n, x, dom, ran, _) => pushF env n x dom ran 121 | DFun (n, x, dom, ran, _) => pushF env n x dom ran
122 | DStruct _ => env 122 | DStruct _ => env
123 123
124 fun bbind env x =
125 case ElabEnv.lookupC ElabEnv.basis x of
126 ElabEnv.NotBound => raise Fail "CjrEnv.bbind: Not bound"
127 | ElabEnv.Rel _ => raise Fail "CjrEnv.bbind: Rel"
128 | ElabEnv.Named (n, _) => pushTNamed env x n NONE
129
130 val basis = empty
131 val basis = bbind basis "int"
132 val basis = bbind basis "float"
133 val basis = bbind basis "string"
134
135 end 124 end