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

Agda.Auto.Convert

Documentation

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

type O = (Maybe Int, QName)

data TMode

Constructors

TMAll 

Instances

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

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))

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

freeIn :: Nat -> MExp o -> Bool

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