doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
changeset 30242 aea5d7fa7ef5
parent 26318 967323f93c67
equal deleted inserted replaced
30241:3a1aef73b2b2 30242:aea5d7fa7ef5
     1 structure Nat = 
       
     2 struct
       
     3 
       
     4 datatype nat = Suc of nat | Zero_nat;
       
     5 
       
     6 fun less_nat m (Suc n) = less_eq_nat m n
       
     7   | less_nat n Zero_nat = false
       
     8 and less_eq_nat (Suc m) n = less_nat m n
       
     9   | less_eq_nat Zero_nat n = true;
       
    10 
       
    11 end; (*struct Nat*)
       
    12 
       
    13 structure Codegen = 
       
    14 struct
       
    15 
       
    16 fun in_interval (k, l) n =
       
    17   Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
       
    18 
       
    19 end; (*struct Codegen*)