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