| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.MetaVars.Occurs

Synopsis

class Occurs t where

occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM t

occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term

Documentation

class Occurs t where | Source

Extended occurs check.
Methods

occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM t | Source

Instances

Occurs Sort
Occurs Type
Occurs Term
Occurs a => Occurs ([] a)
Occurs a => Occurs (Arg a)
Occurs a => Occurs (Abs a)
(Occurs a, Occurs b) => Occurs ((,) a b)

occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term | Source

Produced by Haddock version 2.4.2