Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Auto.Convert

Documentation

norm :: Normalise t => t -> TCM t #

type O = (Maybe Int, QName) #

data TMode #

Constructors

TMAll 

Instances

Eq TMode # 

Methods

(==) :: TMode -> TMode -> Bool #

(/=) :: TMode -> TMode -> Bool #

type MapS a b = (Map a b, [a]) #

initMapS :: MapS a b #

popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b) #

data S #

type TOM = StateT S TCM #

tomy :: MetaId -> [(Bool, QName)] -> [Type] -> TCM ([ConstRef O], [MExp O], Map MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]), [(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O)) #

tomyClauses :: [Clause] -> TOM [([Pat O], MExp O)] #

weaken :: Int -> MExp O -> MExp O #

cnvh :: LensHiding a => a -> FMode #

freeIn :: Nat -> MExp o -> Bool #

negtype :: ConstRef o -> MExp o -> MExp o #

matchType :: Int -> Int -> Type -> Type -> Maybe (Nat, Nat) #