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