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

Agda.TypeChecking.Rules.LHS.Implicit

Synopsis

# Documentation

Insert implicit patterns in a problem.

Eta-expand implicit pattern if of record type.

Try to eta-expand implicit pattern. Returns Nothing unless dealing with a record type that has eta-expansion and a constructor c. In this case, it returns Just c _ _ ... _ (record constructor applied to as many implicit patterns as there are fields).

Insert implicit patterns in a list of patterns. Even if DontExpandLast, trailing SIZELT patterns are inserted.

Insert trailing SizeLt patterns, if any.

Insert implicit patterns in a list of patterns. Even if DontExpandLast, trailing SIZELT patterns are inserted.