namespace http://cds.omdoc.org/urtheories

theory PL =
   oftype   # : 1

   List     # List 1
   list     # [ 1, ]
   
   Option   # Option 1
   some     # some 1
   none     # none
   
   Tuple    # 1× 
   tuple    #  1,  
   proj     # 1 . 2
   
   Function # 1×  2
   lambda   # λ V1T, . -2 prec 20
   apply    # 1@
   
   Nat   # 
   plus  # 1+
   times # 1*
   minus # 1 - 2
   div   # 1 / 2
   less      # 1 < 2
   lesseq    # 1  2
   greater   # 1 > 2
   greatereq # 1  2
   
   Boolean # 
   and     # 1
   or      # 1
   equal   # 1 = 2
   ifte    # if ( 1 ) 2 else 3

   match   # 1 match 2| prec 50
   case    # [ V2T, ] 1  3 prec 5