module Model.Config

family ModelWord32 : Type 0
constructor ModelWord32Value
field unrestricted modelWord32Byte0 : Byte
field unrestricted modelWord32Byte1 : Byte
field unrestricted modelWord32Byte2 : Byte
field unrestricted modelWord32Byte3 : Byte

end-family

family ModelBoolean : Type 0
constructor ModelFalse
constructor ModelTrue

end-family

def modelWord32 =
  (lambda unrestricted byte0 : Byte .
    (lambda unrestricted byte1 : Byte .
      (lambda unrestricted byte2 : Byte .
        (lambda unrestricted byte3 : Byte .
          (constructor ModelWord32 ModelWord32Value byte0 byte1 byte2 byte3)))))

def modelWord32Bytes =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted motiveValue : (family ModelWord32) . Bytes)
      value
      (branch
        ModelWord32Value
        byte0
        byte1
        byte2
        byte3
        .
        (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b"")))))))

def modelWord32One =
  (constructor ModelWord32 ModelWord32Value (byte 1) (byte 0) (byte 0) (byte 0))

def modelWord32Four =
  (constructor ModelWord32 ModelWord32Value (byte 4) (byte 0) (byte 0) (byte 0))

def modelWord32Sixteen =
  (constructor ModelWord32 ModelWord32Value (byte 16) (byte 0) (byte 0) (byte 0))

def modelWord32SixtyFour =
  (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0))

def modelWord32TwoHundredFiftySix =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 1) (byte 0) (byte 0))

def modelWord32OneThousandTwentyFour =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 4) (byte 0) (byte 0))

def modelWord32FourThousandNinetySix =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 16) (byte 0) (byte 0))

def modelWord32TenThousandTwoHundredForty =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 40) (byte 0) (byte 0))

def modelWord32TwelveThousandTwoHundredEightyEight =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 48) (byte 0) (byte 0))