packages feed

Agda-2.3.2.2: src/transl/agda/MetaVars.hs

module MetaVars where
type MetaVar = Int

preMetaVar :: MetaVar
preMetaVar = -1

type ParseInfo = Bool

type Visibility = Maybe Bool
-- Nothing means that the metavariable isn't visible
-- Just aut menas that the metavariable is visible and the
-- bool aut indicates if it should be automatically solved or not, i.e. an _ metavariable.

isAutomatic Nothing = True  -- a hidden metavariable should be automatically solved
isAutomatic (Just aut) = aut

mkAutomatic Nothing = Nothing
mkAutomatic (Just _) = Just True

isVisible Nothing = False
isVisible _ = True

isVisAut Nothing = False
isVisAut (Just aut) = aut