Mercurial > urweb
comparison src/elab_env.sig @ 171:c7a6e6dbc318
Elaborating some basic pattern matching
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 31 Jul 2008 10:06:27 -0400 |
parents | b4b70de488e9 |
children | 7ee424760d2f |
comparison
equal
deleted
inserted
replaced
170:a158f8c5aa55 | 171:c7a6e6dbc318 |
---|---|
52 val lookupC : env -> string -> Elab.kind var | 52 val lookupC : env -> string -> Elab.kind var |
53 | 53 |
54 val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env | 54 val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env |
55 type datatyp | 55 type datatyp |
56 val lookupDatatype : env -> int -> datatyp | 56 val lookupDatatype : env -> int -> datatyp |
57 val lookupConstructor : datatyp -> int -> string * Elab.con option | 57 val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option |
58 val constructors : datatyp -> (string * int * Elab.con option) list | 58 val constructors : datatyp -> (string * int * Elab.con option) list |
59 | |
60 val lookupConstructor : env -> string -> (int * Elab.con option * int) option | |
59 | 61 |
60 val pushERel : env -> string -> Elab.con -> env | 62 val pushERel : env -> string -> Elab.con -> env |
61 val lookupERel : env -> int -> string * Elab.con | 63 val lookupERel : env -> int -> string * Elab.con |
62 | 64 |
63 val pushENamed : env -> string -> Elab.con -> env * int | 65 val pushENamed : env -> string -> Elab.con -> env * int |