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

Agda.TypeChecking.Injectivity

Synopsis

# Documentation

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

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

Join a list of inversion maps.

Update the heads of an inversion map.

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 _,_.

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.

Argument should be in weak head normal form.

data InvView Source #

Constructors

 Inv QName [Elim] (InversionMap Clause) NoInv

Constructors

 Abort KeepGoing

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.