1 
    2 module Tags 
    3 where
    4 
    5 import Parse
    6 
    7 import Build_Tm
    8 
    9 import Unparse
   10 
   11 import Build_itrm
   12 
   13 import Token
   14 
   15 import Type_defs
   16 
   17 import Kernel
   18 
   19 import Core_datatype
   20 
   21 import Vtslib
   22 
   23 type Tag_table = [ Tag ]
   24 
   25 tgL = ( [ ("reflex" , [ Term_Arg ]            , [ Thm_Fn reflex_fn ] ) ,
   26           ("\226"   , [ Deriv_Arg , Int_Arg ] , [ Thm_Fn beta_fn ] ) ,
   27           ("\232"   , [ Deriv_Arg , Int_Arg ] , [ Thm_Fn eta_fn ] ) ,
   28           ("symmetry", [ Deriv_Arg ]          , [ Thm_Fn symmetry_fn ] ) ,
   29           ("\186"   , [ Term_Arg ]            , [ Thm_Fn taut_fn ] ) ,
   30           ("if_true" , [ Deriv_Arg , Deriv_Arg , Int_Arg ] , [ Thm_Fn if_true_fn] )
   31             ])
   32 
   33 reflex_fn [ Tg_Trm tm ] = reflex tm
   34 
   35 beta_fn [ Tg_Thm th , Tg_Int iL ] = beta_rw th iL
   36 
   37 eta_fn [ Tg_Thm th , Tg_Int iL ] = eta_rw th iL
   38 
   39 symmetry_fn [ Tg_Thm th ] = symmetry th
   40 
   41 taut_fn [ Tg_Trm tm ] = taut tm
   42 
   43 if_true_fn [ Tg_Thm th1 , Tg_Thm th2 , Tg_Int iL ] = cond_true_rw th1 th2 iL
   44 
   45 
   46 
   47 default_tag_tbl = tgL
   48