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

Agda.TypeChecking.MetaVars.Occurs

Synopsis

- data OccursCtx
  - = Flex
  - | Rigid
- abort :: OccursCtx -> TypeError -> TCM ()
- class Occurs t where
  - occurs :: OccursCtx -> MetaId -> [Nat] -> t -> TCM t
- occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term
- hasBadRigid :: [Nat] -> Term -> Bool
- killArgs :: [Bool] -> MetaId -> TCM Bool
- killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)
- performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()

# Documentation

data OccursCtx

Constructors

Flex |
Rigid |

Instances

Eq OccursCtx |
Show OccursCtx |

abort :: OccursCtx -> TypeError -> TCM ()

class Occurs t where

Extended occurs check.

Methods

occurs :: OccursCtx -> MetaId -> [Nat] -> t -> TCM t

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

When assigning `m xs := v`, check that `m` does not occur in `v` and that the free variables of `v` are contained in `xs`.

hasBadRigid :: [Nat] -> Term -> Bool

killArgs :: [Bool] -> MetaId -> TCM Bool

killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)

performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()