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

Safe HaskellNone
LanguageHaskell98

Agda.Auto.Convert

Documentation

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

type O = (Maybe Int, QName) Source

data TMode Source

Constructors

TMAll 

Instances

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

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