TFL/thry.sig
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
equal deleted inserted replaced
3244:71b760618f30 3245:241838c01caf
     1 signature Thry_sig =
     1 signature Thry_sig =
     2 sig
     2 sig
     3   type Type
       
     4   type Preterm
       
     5   type Term
       
     6   type Thm
       
     7   type Thry
       
     8   type 'a binding
     3   type 'a binding
     9 
     4 
    10   structure USyntax : USyntax_sig
     5   structure USyntax : USyntax_sig
    11   val match_term : Thry -> Preterm -> Preterm 
     6   val match_term : theory -> term -> term 
    12                     -> Preterm binding list * Type binding list
     7                     -> term binding list * typ binding list
    13 
     8 
    14   val match_type : Thry -> Type -> Type -> Type binding list
     9   val match_type : theory -> typ -> typ -> typ binding list
    15 
    10 
    16   val typecheck : Thry -> Preterm -> Term
    11   val typecheck : theory -> term -> cterm
    17 
    12 
    18   val make_definition: Thry -> string -> Preterm -> Thm * Thry
    13   val make_definition: theory -> string -> term -> thm * theory
    19 
    14 
    20   (* Datatype facts of various flavours *)
    15   (* Datatype facts of various flavours *)
    21   val match_info: Thry -> string -> {constructors:Preterm list,
    16   val match_info: theory -> string -> {constructors:term list,
    22                                      case_const:Preterm} USyntax.Utils.option
    17                                      case_const:term} option
    23 
    18 
    24   val induct_info: Thry -> string -> {constructors:Preterm list,
    19   val induct_info: theory -> string -> {constructors:term list,
    25                                       nchotomy:Thm} USyntax.Utils.option
    20                                       nchotomy:thm} option
    26 
    21 
    27   val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
    22   val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
    28 
    23 
    29 end;
    24 end;
    30 
    25 
    31 
    26