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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Injectivity

Synopsis

Documentation

headSymbol' :: Term -> TCM (Maybe TermHead) Source #

Do a full whnf and treat neutral terms as rigid. Used on the arguments to an injective functions and to the right-hand side.

topLevelArg :: Clause -> Int -> Maybe TermHead Source #

Does deBruijn variable i correspond to a top-level argument, and if so which one (index from the left).

joinHeadMaps :: [InversionMap c] -> InversionMap c Source #

Join a list of inversion maps.

updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c) Source #

Update the heads of an inversion map.

checkOverapplication :: Elims -> InversionMap Clause -> TCM (InversionMap Clause) Source #

If a clause is over-applied we can't trust the head (Issue 2944). For instance, the clause might be `f ps = u , v` and the actual call `f vs .fst`. In this case the head will be the head of u rather than `_,_`.

instantiateVarHeads :: QName -> Elims -> InversionMap c -> TCM (Maybe (InversionMap c)) Source #

Turn variable heads, referring to top-level argument positions, into proper heads. These might still be VarHead, but in that case they refer to deBruijn variables. Checks that the instantiated heads are still rigid and distinct.

functionInverse :: Term -> TCM InvView Source #

Argument should be in weak head normal form.

data MaybeAbort Source #

Constructors

Abort 
KeepGoing 

useInjectivity :: CompareDirection -> Type -> Term -> Term -> TCM () Source #

Precondition: The first argument must be blocked and the second must be neutral.

invertFunction :: Comparison -> Term -> InvView -> TermHead -> TCM () -> TCM () -> (Term -> TCM ()) -> TCM () Source #

The second argument should be a blocked application and the third argument the inverse of the applied function.