Nominal/nominal_dt_rawfuns.ML
changeset 2375 e163fd99de44
parent 2321 e9b0728061a8
child 2384 841b7e34e70a
equal deleted inserted replaced
2374:0321e89e66a3 2375:e163fd99de44
    33 
    33 
    34 
    34 
    35 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
    35 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
    36 struct
    36 struct
    37 
    37 
       
    38 (* term              - is constant of the bn-function 
       
    39    int               - is datatype number over which the bn-function is defined
       
    40    int * term option - is number of the corresponding argument with possibly
       
    41                        recursive call with bn-function term 
       
    42 *)  
    38 type bn_info = (term * int * (int * term option) list list) list
    43 type bn_info = (term * int * (int * term option) list list) list
    39 
    44 
    40 datatype bmode = Lst | Res | Set
    45 datatype bmode = Lst | Res | Set
    41 datatype bclause = BC of bmode * (term option * int) list * int list
    46 datatype bclause = BC of bmode * (term option * int) list * int list
    42 
    47