TFL/thry.sig
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
signature Thry_sig =
paulson@2112
     2
sig
paulson@2112
     3
  type Type
paulson@2112
     4
  type Preterm
paulson@2112
     5
  type Term
paulson@2112
     6
  type Thm
paulson@2112
     7
  type Thry
paulson@2112
     8
  type 'a binding
paulson@2112
     9
paulson@2112
    10
  structure USyntax : USyntax_sig
paulson@2112
    11
  val match_term : Thry -> Preterm -> Preterm 
paulson@2112
    12
                    -> Preterm binding list * Type binding list
paulson@2112
    13
paulson@2112
    14
  val match_type : Thry -> Type -> Type -> Type binding list
paulson@2112
    15
paulson@2112
    16
  val typecheck : Thry -> Preterm -> Term
paulson@2112
    17
paulson@2112
    18
  val make_definition: Thry -> string -> Preterm -> Thm * Thry
paulson@2112
    19
paulson@2112
    20
  (* Datatype facts of various flavours *)
paulson@2112
    21
  val match_info: Thry -> string -> {constructors:Preterm list,
paulson@2112
    22
                                     case_const:Preterm} USyntax.Utils.option
paulson@2112
    23
paulson@2112
    24
  val induct_info: Thry -> string -> {constructors:Preterm list,
paulson@2112
    25
                                      nchotomy:Thm} USyntax.Utils.option
paulson@2112
    26
paulson@2112
    27
  val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
paulson@2112
    28
paulson@2112
    29
end;
paulson@2112
    30
paulson@2112
    31