{-# OPTIONS_GHC -Wno-missing-import-lists #-}
module Grisette.Utils
(
unsafeAxiom,
NatRepr,
natValue,
natRepr,
decNat,
predNat,
incNat,
addNat,
subNat,
divNat,
halfNat,
KnownProof (..),
hasRepr,
withKnownProof,
unsafeKnownProof,
knownAdd,
LeqProof (..),
withLeqProof,
unsafeLeqProof,
testLeq,
leqRefl,
leqSucc,
leqTrans,
leqZero,
leqAdd2,
leqAdd,
leqAddPos,
)
where
import Grisette.Internal.Utils.Parameterized
( KnownProof (..),
LeqProof (..),
NatRepr,
addNat,
decNat,
divNat,
halfNat,
hasRepr,
incNat,
knownAdd,
leqAdd,
leqAdd2,
leqAddPos,
leqRefl,
leqSucc,
leqTrans,
leqZero,
natRepr,
natValue,
predNat,
subNat,
testLeq,
unsafeAxiom,
unsafeKnownProof,
unsafeLeqProof,
withKnownProof,
withLeqProof,
)