Mercurial > urweb

comparison src/elab_env.sig @ 9:14b533dbe6cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added simple expression constructors to Elab
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 17:26:14 -0500
parents 258261a53842
children e97c6d335869
comparison
equal deleted inserted replaced
8:a455a9f85cc3 9:14b533dbe6cc
32 val empty : env 32 val empty : env
33 33
34 exception UnboundRel of int 34 exception UnboundRel of int
35 exception UnboundNamed of int 35 exception UnboundNamed of int
36 36
37 datatype 'a var =
38 NotBound
39 | Rel of int * 'a
40 | Named of int * 'a
41
37 val pushCRel : env -> string -> Elab.kind -> env 42 val pushCRel : env -> string -> Elab.kind -> env
38 val lookupCRel : env -> int -> string * Elab.kind 43 val lookupCRel : env -> int -> string * Elab.kind
39 44
40 val pushCNamed : env -> string -> Elab.kind -> env * int 45 val pushCNamed : env -> string -> Elab.kind -> env * int
41 val pushCNamedAs : env -> string -> int -> Elab.kind -> env 46 val pushCNamedAs : env -> string -> int -> Elab.kind -> env
42 val lookupCNamed : env -> int -> string * Elab.kind 47 val lookupCNamed : env -> int -> string * Elab.kind
48
49 val lookupC : env -> string -> Elab.kind var
50
51 val pushERel : env -> string -> Elab.con -> env
52 val lookupERel : env -> int -> string * Elab.con
53
54 val pushENamed : env -> string -> Elab.con -> env * int
55 val pushENamedAs : env -> string -> int -> Elab.con -> env
56 val lookupENamed : env -> int -> string * Elab.con
43 57
44 datatype var = 58 val lookupE : env -> string -> Elab.con var
45 CNotBound
46 | CRel of int * Elab.kind
47 | CNamed of int * Elab.kind
48 val lookupC : env -> string -> var
49 59
50 end 60 end