Conversion.hs-boot

module Agda.TypeChecking.Conversion where

import Agda.Syntax.Internal
import Agda.TypeChecking.Monad

compareTerm  :: Comparison -> Type -> Term -> Term -> TCM ()
compareTermOnFace :: Comparison -> Term -> Type -> Term -> Term -> TCM ()
compareAtom  :: Comparison -> Type -> Term -> Term -> TCM ()
compareArgs  :: [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> TCM ()
compareElims :: [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
compareType  :: Comparison -> Type -> Type -> TCM ()
compareTel   :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()
compareSort  :: Comparison -> Sort -> Sort -> TCM ()
compareLevel :: Comparison -> Level -> Level -> TCM ()
equalTerm    :: Type -> Term -> Term -> TCM ()
equalTermOnFace :: Term -> Type -> Term -> Term -> TCM ()
equalType    :: Type -> Type -> TCM ()
equalSort    :: Sort -> Sort -> TCM ()
equalLevel   :: Level -> Level -> TCM ()
leqType      :: Type -> Type -> TCM ()
leqLevel     :: Level -> Level -> TCM ()