TFL/thry.sig

improved messages;

signature Thry_sig =
sig
  type Type
  type Preterm
  type Term
  type Thm
  type Thry
  type 'a binding

  structure USyntax : USyntax_sig
  val match_term : Thry -> Preterm -> Preterm 
                    -> Preterm binding list * Type binding list

  val match_type : Thry -> Type -> Type -> Type binding list

  val typecheck : Thry -> Preterm -> Term

  val make_definition: Thry -> string -> Preterm -> Thm * Thry

  (* Datatype facts of various flavours *)
  val match_info: Thry -> string -> {constructors:Preterm list,
                                     case_const:Preterm} USyntax.Utils.option

  val induct_info: Thry -> string -> {constructors:Preterm list,
                                      nchotomy:Thm} USyntax.Utils.option

  val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}

end;