Library CFML.Stdlib.Sys_ml

Set Implicit Arguments.

Require Coq.ZArith.BinInt TLC.LibLogic TLC.LibRelation TLC.LibInt TLC.LibListZ CFML.Shared CFML.CFHeaps CFML.CFApp CFML.CFPrint CFML.CFBuiltin.

Require Import Coq.ZArith.BinIntDef CFML.CFHeader.

Delimit Scope Z_scope with Z.

Local Open Scope cfheader_scope.

Parameter big_endian : Coq.Init.Datatypes.bool.

Parameter big_endian__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_val (
    Coq.Init.Logic.eq big_endian (
      (Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool) : Coq.Init.Datatypes.bool
    )
  ).

Hint Extern 1 (RegisterCF big_endian) => CFHeader_Provide big_endian__cf.

Parameter word_size : Coq.ZArith.BinInt.Z.

Parameter word_size__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_val (
    Coq.Init.Logic.eq word_size ((64)%Z : Coq.ZArith.BinInt.Z)
  ).

Hint Extern 1 (RegisterCF word_size) => CFHeader_Provide word_size__cf.

Parameter max_array_length : Coq.ZArith.BinInt.Z.

Parameter max_array_length__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_val (
    Coq.Init.Logic.eq max_array_length (
      (18014398509481983)%Z : Coq.ZArith.BinInt.Z
    )
  ).

Hint Extern 1 (RegisterCF max_array_length) => CFHeader_Provide max_array_length__cf.

Parameter max_string_length : Coq.ZArith.BinInt.Z.

Parameter max_string_length__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_val (
    Coq.Init.Logic.eq max_string_length (
      (144115188075855863)%Z : Coq.ZArith.BinInt.Z
    )
  ).

Hint Extern 1 (RegisterCF max_string_length) => CFHeader_Provide max_string_length__cf.