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

Agda.Syntax.Internal.Pattern

Synopsis

# Tools for clauses

Translate the clause patterns to terms with free variables bound by the clause telescope.

Precondition: no projection patterns.

Translate the clause patterns to an elimination spine with free variables bound by the clause telescope.

class FunArity a where Source #

Arity of a function, computed from clauses.

Minimal complete definition

funArity

Methods

funArity :: a -> Int Source #

Instances

 Source # Get the number of initial Apply patterns in a clause. Methods IsProjP p => FunArity [p] Source # Get the number of initial Apply patterns. MethodsfunArity :: [p] -> Int Source # Source # Get the number of common initial Apply patterns in a list of clauses. MethodsfunArity :: [Clause] -> Int Source #

# Tools for patterns

class LabelPatVars a b i | b -> i where Source #

Label the pattern variables from left to right using one label for each variable pattern and one for each dot pattern.

Minimal complete definition

Methods

labelPatVars :: a -> State [i] b Source #

unlabelPatVars :: b -> a Source #

Intended, but unpractical due to the absence of type-level lambda, is: labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))

Instances

 LabelPatVars a b i => LabelPatVars [a] [b] i Source # MethodslabelPatVars :: [a] -> State [i] [b] Source #unlabelPatVars :: [b] -> [a] Source # LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i Source # MethodslabelPatVars :: Arg a -> State [i] (Arg b) Source #unlabelPatVars :: Arg b -> Arg a Source # LabelPatVars (Pattern' x) (Pattern' (i, x)) i Source # MethodslabelPatVars :: Pattern' x -> State [i] (Pattern' (i, x)) Source #unlabelPatVars :: Pattern' (i, x) -> Pattern' x Source # LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i Source # MethodslabelPatVars :: Named x a -> State [i] (Named x b) Source #unlabelPatVars :: Named x b -> Named x a Source #

numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b Source #

Augment pattern variables with their de Bruijn index.