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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Rules.LHS.Problem

Contents

- Orphan instances

Synopsis

- type FlexibleVars = [FlexibleVar Nat]
- data FlexibleVarKind
  - = RecordFlex [FlexibleVarKind]
  - | ImplicitFlex
  - | DotFlex
  - | OtherFlex
- data FlexibleVar a = FlexibleVar {
  - flexArgInfo :: ArgInfo
  - flexForced :: IsForced
  - flexKind :: FlexibleVarKind
  - flexPos :: Maybe Int
  - flexVar :: a
  }
- allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
- data FlexChoice
  - = ChooseLeft
  - | ChooseRight
  - | ChooseEither
  - | ExpandBoth
- class ChooseFlex a where
  - chooseFlex :: a -> a -> FlexChoice
- data ProblemEq = ProblemEq {
  - problemInPat :: Pattern
  - problemInst :: Term
  - problemType :: Dom Type
  }
- data Problem a = Problem {
  - _problemEqs :: [ProblemEq]
  - _problemRestPats :: [NamedArg Pattern]
  - _problemCont :: LHSState a -> TCM a
  }
- problemEqs :: Lens' [ProblemEq] (Problem a)
- problemRestPats :: Lens' [NamedArg Pattern] (Problem a)
- problemCont :: Lens' (LHSState a -> TCM a) (Problem a)
- problemInPats :: Problem a -> [Pattern]
- data AsBinding = AsB Name Term Type Modality
- data DotPattern = Dot Expr Term (Dom Type)
- data AbsurdPattern = Absurd Range Type
- data AnnotationPattern = Ann Expr Type
- data LHSState a = LHSState {
  - _lhsTel :: Telescope
  - _lhsOutPat :: [NamedArg DeBruijnPattern]
  - _lhsProblem :: Problem a
  - _lhsTarget :: Arg Type
  - _lhsPartialSplit :: ![Maybe Int]
  }
- lhsTel :: Lens' Telescope (LHSState a)
- lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a)
- lhsProblem :: Lens' (Problem a) (LHSState a)
- lhsTarget :: Lens' (Arg Type) (LHSState a)
- data LeftoverPatterns = LeftoverPatterns {
  - patternVariables :: IntMap [(Name, PatVarPosition)]
  - asPatterns :: [AsBinding]
  - dotPatterns :: [DotPattern]
  - absurdPatterns :: [AbsurdPattern]
  - typeAnnotations :: [AnnotationPattern]
  - otherPatterns :: [Pattern]
  }
- getLeftoverPatterns :: forall m. PureTCM m => [ProblemEq] -> m LeftoverPatterns
- getUserVariableNames :: Telescope -> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])

# Documentation

type FlexibleVars = [FlexibleVar Nat] Source #

data FlexibleVarKind Source #

When we encounter a flexible variable in the unifier, where did it come from? The alternatives are ordered such that we will assign the higher one first, i.e., first we try to assign a `DotFlex`, then...

Constructors

RecordFlex [FlexibleVarKind] | From a record pattern (`ConP`). Saves the `FlexibleVarKind` of its subpatterns.
ImplicitFlex | From a hidden formal argument or underscore (`WildP`).
DotFlex | From a dot pattern (`DotP`).
OtherFlex | From a non-record constructor or literal (`ConP` or `LitP`).

#### Instances

Instances details

ChooseFlex FlexibleVarKind Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice Source #
Show FlexibleVarKind Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexibleVarKind -> ShowS Source # show :: FlexibleVarKind -> String Source # showList :: [FlexibleVarKind] -> ShowS Source #
Eq FlexibleVarKind Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexibleVarKind -> FlexibleVarKind -> Bool Source # (/=) :: FlexibleVarKind -> FlexibleVarKind -> Bool Source #

data FlexibleVar a Source #

Flexible variables are equipped with information where they come from, in order to make a choice which one to assign when two flexibles are unified.

Constructors

FlexibleVar |

Fields

- flexArgInfo :: ArgInfo
- flexForced :: IsForced
- flexKind :: FlexibleVarKind
- flexPos :: Maybe Int
- flexVar :: a

#### Instances

Instances details

Foldable FlexibleVar Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

fold :: Monoid m => FlexibleVar m -> m Source #

foldMap :: Monoid m => (a -> m) -> FlexibleVar a -> m Source #

foldMap' :: Monoid m => (a -> m) -> FlexibleVar a -> m Source #

foldr :: (a -> b -> b) -> b -> FlexibleVar a -> b Source #

foldr' :: (a -> b -> b) -> b -> FlexibleVar a -> b Source #

foldl :: (b -> a -> b) -> b -> FlexibleVar a -> b Source #

foldl' :: (b -> a -> b) -> b -> FlexibleVar a -> b Source #

foldr1 :: (a -> a -> a) -> FlexibleVar a -> a Source #

foldl1 :: (a -> a -> a) -> FlexibleVar a -> a Source #

toList :: FlexibleVar a -> [a] Source #

null :: FlexibleVar a -> Bool Source #

length :: FlexibleVar a -> Int Source #

elem :: Eq a => a -> FlexibleVar a -> Bool Source #

maximum :: Ord a => FlexibleVar a -> a Source #

minimum :: Ord a => FlexibleVar a -> a Source #

sum :: Num a => FlexibleVar a -> a Source #

product :: Num a => FlexibleVar a -> a Source #

Traversable FlexibleVar Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods traverse :: Applicative f => (a -> f b) -> FlexibleVar a -> f (FlexibleVar b) Source # sequenceA :: Applicative f => FlexibleVar (f a) -> f (FlexibleVar a) Source # mapM :: Monad m => (a -> m b) -> FlexibleVar a -> m (FlexibleVar b) Source # sequence :: Monad m => FlexibleVar (m a) -> m (FlexibleVar a) Source #
Functor FlexibleVar Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods fmap :: (a -> b) -> FlexibleVar a -> FlexibleVar b Source # (<$) :: a -> FlexibleVar b -> FlexibleVar a Source #
LensArgInfo (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getArgInfo :: FlexibleVar a -> ArgInfo Source # setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a Source #
LensHiding (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getHiding :: FlexibleVar a -> Hiding Source # setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a Source # mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a Source #
LensModality (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getModality :: FlexibleVar a -> Modality Source # setModality :: Modality -> FlexibleVar a -> FlexibleVar a Source # mapModality :: (Modality -> Modality) -> FlexibleVar a -> FlexibleVar a Source #
LensOrigin (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getOrigin :: FlexibleVar a -> Origin Source # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a Source # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a Source #
ChooseFlex a => ChooseFlex (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice Source #
Show a => Show (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexibleVar a -> ShowS Source # show :: FlexibleVar a -> String Source # showList :: [FlexibleVar a] -> ShowS Source #
Eq a => Eq (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexibleVar a -> FlexibleVar a -> Bool Source # (/=) :: FlexibleVar a -> FlexibleVar a -> Bool Source #

allFlexVars :: [IsForced] -> Telescope -> FlexibleVars Source #

data FlexChoice Source #

Constructors

ChooseLeft |
ChooseRight |
ChooseEither |
ExpandBoth |

#### Instances

Instances details

Monoid FlexChoice Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods mempty :: FlexChoice Source # mappend :: FlexChoice -> FlexChoice -> FlexChoice Source # mconcat :: [FlexChoice] -> FlexChoice Source #
Semigroup FlexChoice Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: FlexChoice -> FlexChoice -> FlexChoice Source # sconcat :: NonEmpty FlexChoice -> FlexChoice Source # stimes :: Integral b => b -> FlexChoice -> FlexChoice Source #
Show FlexChoice Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexChoice -> ShowS Source # show :: FlexChoice -> String Source # showList :: [FlexChoice] -> ShowS Source #
Eq FlexChoice Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexChoice -> FlexChoice -> Bool Source # (/=) :: FlexChoice -> FlexChoice -> Bool Source #

class ChooseFlex a where Source #

Methods

chooseFlex :: a -> a -> FlexChoice Source #

#### Instances

Instances details

ChooseFlex ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source #
ChooseFlex Hiding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source #
ChooseFlex Origin Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice Source #
ChooseFlex IsForced Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: IsForced -> IsForced -> FlexChoice Source #
ChooseFlex FlexibleVarKind Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice Source #
ChooseFlex Int Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Int -> Int -> FlexChoice Source #
ChooseFlex a => ChooseFlex (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice Source #
ChooseFlex a => ChooseFlex (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Maybe a -> Maybe a -> FlexChoice Source #
ChooseFlex a => ChooseFlex [a] Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: [a] -> [a] -> FlexChoice Source #

data ProblemEq Source #

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Constructors

ProblemEq |

Fields

- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type

#### Instances

Instances details

KillRange ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq Source #
PrettyTCM ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
Subst ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg ProblemEq Source # Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #
Data ProblemEq Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq Source #

toConstr :: ProblemEq -> Constr Source #

dataTypeOf :: ProblemEq -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) Source #

gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq Source #

Generic ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ProblemEq :: Type -> Type Source # Methods from :: ProblemEq -> Rep ProblemEq x Source # to :: Rep ProblemEq x -> ProblemEq Source #
Show ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ProblemEq -> ShowS Source # show :: ProblemEq -> String Source # showList :: [ProblemEq] -> ShowS Source #
NFData ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ProblemEq -> () Source #
Eq ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ProblemEq -> ProblemEq -> Bool Source # (/=) :: ProblemEq -> ProblemEq -> Bool Source #
type SubstArg ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term
type Rep ProblemEq Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

data Problem a Source #

The user patterns we still have to split on.

Constructors

Problem |

Fields

- _problemEqs :: [ProblemEq]

  User patterns which are typed (including the ones generated from implicit arguments).

- _problemRestPats :: [NamedArg Pattern]

  List of user patterns which could not yet be typed. Example: `f : (b : Bool) -> if b then Nat else Nat -> Nat f true = zero f false zero = zero f false (suc n) = n` In this sitation, for clause 2, we construct an initial problem `problemEqs = [false = b] problemRestPats = [zero]` As we instantiate `b` to `false`, the `targetType` reduces to `Nat -> Nat` and we can move pattern `zero` over to `problemEqs`.

- _problemCont :: LHSState a -> TCM a

  The code that checks the RHS.

#### Instances

Instances details

Subst (Problem a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Associated Types type SubstArg (Problem a) Source # Methods applySubst :: Substitution' (SubstArg (Problem a)) -> Problem a -> Problem a Source #
Show (Problem a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> Problem a -> ShowS Source # show :: Problem a -> String Source # showList :: [Problem a] -> ShowS Source #
type SubstArg (Problem a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg (Problem a) = Term

problemEqs :: Lens' [ProblemEq] (Problem a) Source #

problemRestPats :: Lens' [NamedArg Pattern] (Problem a) Source #

problemCont :: Lens' (LHSState a -> TCM a) (Problem a) Source #

problemInPats :: Problem a -> [Pattern] Source #

data AsBinding Source #

Constructors

AsB Name Term Type Modality |

#### Instances

Instances details

PrettyTCM AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AsBinding -> m Doc Source #
InstantiateFull AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods instantiateFull' :: AsBinding -> ReduceM AsBinding Source #
Subst AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Associated Types type SubstArg AsBinding Source # Methods applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding Source #
Pretty AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods pretty :: AsBinding -> Doc Source # prettyPrec :: Int -> AsBinding -> Doc Source # prettyList :: [AsBinding] -> Doc Source #
type SubstArg AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AsBinding = Term

data DotPattern Source #

Constructors

Dot Expr Term (Dom Type) |

#### Instances

Instances details

PrettyTCM DotPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => DotPattern -> m Doc Source #
Subst DotPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Associated Types type SubstArg DotPattern Source # Methods applySubst :: Substitution' (SubstArg DotPattern) -> DotPattern -> DotPattern Source #
type SubstArg DotPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg DotPattern = Term

data AbsurdPattern Source #

Constructors

Absurd Range Type |

#### Instances

Instances details

PrettyTCM AbsurdPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc Source #
Subst AbsurdPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Associated Types type SubstArg AbsurdPattern Source # Methods applySubst :: Substitution' (SubstArg AbsurdPattern) -> AbsurdPattern -> AbsurdPattern Source #
type SubstArg AbsurdPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AbsurdPattern = Term

data AnnotationPattern Source #

Constructors

Ann Expr Type |

#### Instances

Instances details

PrettyTCM AnnotationPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc Source #

data LHSState a Source #

State worked on during the main loop of checking a lhs. [Ulf Norell's PhD, page. 35]

Constructors

LHSState |

Fields

- _lhsTel :: Telescope

  The types of the pattern variables.

- _lhsOutPat :: [NamedArg DeBruijnPattern]

  Patterns after splitting. The de Bruijn indices refer to positions in the list of abstract syntax patterns in the problem, counted from the back (right-to-left).

- _lhsProblem :: Problem a

  User patterns of supposed type `delta`.

- _lhsTarget :: Arg Type

  Type eliminated by `problemRestPats` in the problem. Can be `Irrelevant` to indicate that we came by an irrelevant projection and, hence, the rhs must be type-checked in irrelevant mode.

- _lhsPartialSplit :: ![Maybe Int]

  have we splitted with a PartialFocus?

#### Instances

Instances details

PrettyTCM (LHSState a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LHSState a -> m Doc Source #

lhsTel :: Lens' Telescope (LHSState a) Source #

lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a) Source #

lhsProblem :: Lens' (Problem a) (LHSState a) Source #

lhsTarget :: Lens' (Arg Type) (LHSState a) Source #

data LeftoverPatterns Source #

Constructors

LeftoverPatterns |

Fields

- patternVariables :: IntMap [(Name, PatVarPosition)]
- asPatterns :: [AsBinding]
- dotPatterns :: [DotPattern]
- absurdPatterns :: [AbsurdPattern]
- typeAnnotations :: [AnnotationPattern]
- otherPatterns :: [Pattern]

#### Instances

Instances details

PrettyTCM LeftoverPatterns Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc Source #
Null LeftoverPatterns Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods empty :: LeftoverPatterns Source # null :: LeftoverPatterns -> Bool Source #
Monoid LeftoverPatterns Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods mempty :: LeftoverPatterns Source # mappend :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns Source # mconcat :: [LeftoverPatterns] -> LeftoverPatterns Source #
Semigroup LeftoverPatterns Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns Source # sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns Source # stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns Source #

getLeftoverPatterns :: forall m. PureTCM m => [ProblemEq] -> m LeftoverPatterns Source #

Classify remaining patterns after splitting is complete into pattern variables, as patterns, dot patterns, and absurd patterns. Precondition: there are no more constructor patterns.

getUserVariableNames Source #

Arguments

:: Telescope | The telescope of pattern variables
-> IntMap [(Name, PatVarPosition)] | The list of user names for each pattern variable
-> ([Maybe Name], [AsBinding]) |

Build a renaming for the internal patterns using variable names from the user patterns. If there are multiple user names for the same internal variable, the unused ones are returned as as-bindings. Names that are not also module parameters are preferred over those that are.

# Orphan instances

PrettyTCM ProblemEq Source # |
Instance details Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #