Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument indicates the relevance we are working under: if this is Irrelevant, then we construct a pattern that never fails to match. The second argument is the number of bound variables (from pattern lambdas). The third argument is the type of the term.
Methods
patternFrom :: Relevance -> Int -> TypeOf a -> a -> TCM b
Instances7PatternFrom, …
PatternFrom Level NLPatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPatternPatternFrom Sort NLPSortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPatternPatternFrom Term NLPatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPatternPatternFrom Type NLPTypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPatternPatternFrom Elims [Elim' NLPat]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPatternPatternFrom a b => PatternFrom (Arg a) (Arg b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPatternPatternFrom a b => PatternFrom (Dom a) (Dom b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern