content: {-|
  Copyright        : (c) Galois, Inc 2022
  
  @'FinMap' n a@ conceptually (see NOTE) a map with @'Data.Parameterized.Fin.Fin'
  n@ keys, implying a maximum size of @n@. Here's how 'FinMap' compares to other
  map-like types:
  
  * @'FinMap' n a@ is conceptually isomorphic to a
    @'Data.Parameterized.Vector' n ('Maybe' a)@, but can be more space-efficient
    especially if @n@ is large and the vector is populated with a small number of
    'Just' values.
  * @'FinMap'@ is less general than 'Data.Map.Map', because it has a fixed key
    type (@'Data.Parameterized.Fin.Fin' n@).
  * @'FinMap' n a@ is similar to @'Data.IntMap.IntMap' a@, but it provides a
    static guarantee of a maximum size, and its operations (such as 'size') allow
    the recovery of more type-level information.
  * @'FinMap'@ is dissimilar from "Data.Parameterized.Map.MapF" in that neither
    the key nor value type of 'FinMap' is parameterized.
  
  The type parameter @n@ doesn't track the /current/ number of key-value pairs in
  a @'FinMap' n@ (i.e., the size of the map), but rather /an upper bound/.
  'insert' and 'delete' don't alter @n@, whereas 'incMax' does - despite the fact
  that it has no effect on the keys and values in the 'FinMap'.
  
  The 'FinMap' interface has two implementations:
  
  * The implementation in "Data.Parameterized.FinMap.Unsafe" is backed by an
    'Data.IntMap.IntMap', and must have a size of at most @'maxBound' :: 'Int'@.
    This module uses unsafe operations like 'Unsafe.Coerce.unsafeCoerce'
    internally for the sake of time and space efficiency.
  * The implementation in "Data.Parameterized.FinMap.Safe" is backed by an
    @'Data.Map.Map' ('Data.Parameterized.Fin.Fin' n)@. All of its functions are
    implemented using safe operations.
  
  The implementation in 'Data.Parameterized.FinMap.Unsafe.FinMap' is property
  tested against that in 'Data.Parameterized.FinMap.Safe.FinMap' to ensure
  they have the same behavior.
  
  In this documentation, /W/ is used in big-O notations the same way as in the
  "Data.IntMap" documentation.
  
  NOTE: Where the word "conceptually" is used, it implies that this correspondence
  is not literally true, but is true modulo some details such as differences
  between bounded types like 'Int' and unbounded types like 'Integer'.
  
  Several of the functions in both implementations are marked @INLINE@ or
  @INLINABLE@. There are three reasons for this:
  
  * Some of these just have very small definitions and so inlining is likely more
    beneficial than harmful.
  * Some participate in @RULES@ relevant to functions used in their
    implementations.
  * They are thin wrappers (often just newtype wrappers) around functions marked
    @INLINE@, which should therefore also be inlined.
  -}
  
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Data.Parameterized.FinMap
    (
  #ifdef UNSAFE_OPS
      module Data.Parameterized.FinMap.Unsafe
  #else
      module Data.Parameterized.FinMap.Safe
  #endif
    ) where
  
  #ifdef UNSAFE_OPS
  import Data.Parameterized.FinMap.Unsafe
  #else
  import Data.Parameterized.FinMap.Safe
  #endif
  