module Agda.TypeChecking.UniversePolymorphism where
import Control.Applicative
import Control.Monad.Error
import Data.List
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Level
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Conversion
import qualified Agda.Utils.Warshall as W
import Agda.Utils.Impossible
#include "../undefined.h"
compareLevel :: Comparison -> Level -> Level -> TCM ()
compareLevel CmpLeq u v = leqLevel u v
compareLevel CmpEq u v = equalLevel u v
isLevelConstraint LevelCmp{} = True
isLevelConstraint _ = False