basic.timl

(* Basic types *)

structure Basic = struct

datatype bool = true | false

(* indexed boolean *)                         
datatype ibool : {Bool} =
         True of ibool {true} 
         | False of ibool {false} 

datatype option 'a =
         NONE
         | SOME of 'a --> option 'a 

datatype le {a b : Nat} =
         LE {a <= b} of le {a} {b} 
                   
end