<commit_before>{-@ LIQUID "--exact-data-con"                      @-}
{-@ LIQUID "--higherorder"                         @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

{- NOTE:

   1. See the TODO:trivial for cases where the instances seems to fail

   2. Would be nice to have case-splitting combinatores,
      e.g. for thmAndbCom,  thmAndbExch which are super boilerplate-y

   3. For @minsheng: See the rewritten signature for `thmEqBeq`;
      we don't really need `rewrite` as the SMT
      does "congruence closure" automatically.

 -}

module Basics where

  -- (
    -- -- * Booleans
    -- Bool(..)
  -- , negb, andb, orb
--
    -- -- * Peano numerals
  -- , Peano(..), toNat
  -- , plus, mult
  -- , beq, ble, blt
  -- )
  -- where

import           Prelude (Char, Int)
import qualified Prelude
import           Language.Haskell.Liquid.ProofCombinators

{-@ reflect incr @-}
incr :: Int -> Int
incr x = x Prelude.+ 1

--------------------------------------------------------------------------------
-- | Days ----------------------------------------------------------------------
--------------------------------------------------------------------------------

-- NOTE: clunky to have to redefine this ...

{-@ data Day = Monday
             | Tuesday
             | Wednesday
             | Thursday
             | Friday
             | Saturday
             | Sunday
  @-}<commit_msg>WTF why are sf tests timing out!<commit_after>{-@ LIQUID "--exact-data-con"                      @-}
{-@ LIQUID "--higherorder"                         @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

{- NOTE:

   1. See the TODO:trivial for cases where the instances seems to fail

   2. Would be nice to have case-splitting combinatores,
      e.g. for thmAndbCom,  thmAndbExch which are super boilerplate-y

   3. For @minsheng: See the rewritten signature for `thmEqBeq`;
      we don't really need `rewrite` as the SMT
      does "congruence closure" automatically.

 -}

module Basics where

  -- (
    -- -- * Booleans
    -- Bool(..)
  -- , negb, andb, orb
--
    -- -- * Peano numerals
  -- , Peano(..), toNat
  -- , plus, mult
  -- , beq, ble, blt
  -- )
  -- where

import           Prelude (Char, Int)
import qualified Prelude
import           Language.Haskell.Liquid.ProofCombinators

{-@ reflect incr @-}
incr :: Int -> Int
incr x = x Prelude.+ 1


--------------------------------------------------------------------------------
-- | Days ----------------------------------------------------------------------
--------------------------------------------------------------------------------

-- NOTE: clunky to have to redefine this ...

{-@ data Day = Monday
             | Tuesday
             | Wednesday
             | Thursday
             | Friday
             | Saturday
             | Sunday
  @-}
{'fraction_non_alphanumeric': 0.26917663617171006, 'fraction_numerical': 0.0028149190710767065, 'mean_word_length': 1.102810650887574, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6682599', 'n_tokens_mistral': 822, 'n_tokens_neox': 771, 'n_words': 228}