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

Safe Haskell | None
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 :: forall a f. Functor f => ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a)
- problemRestPats :: forall a f. Functor f => ([NamedArg Pattern] -> f [NamedArg Pattern]) -> Problem a -> f (Problem a)
- problemCont :: forall a f. Functor f => ((LHSState a -> TCM a) -> f (LHSState a -> TCM a)) -> Problem a -> f (Problem a)
- problemInPats :: Problem a -> [Pattern]
- data AsBinding = AsB Name Term (Dom Type)
- 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]
  - _lhsIndexedSplit :: !Bool
  }
- lhsTel :: forall a f. Functor f => (Telescope -> f Telescope) -> LHSState a -> f (LHSState a)
- lhsOutPat :: forall a f. Functor f => ([NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]) -> LHSState a -> f (LHSState a)
- lhsProblem :: forall a f. Functor f => (Problem a -> f (Problem a)) -> LHSState a -> f (LHSState a)
- lhsTarget :: forall a f. Functor f => (Arg Type -> f (Arg Type)) -> LHSState a -> f (LHSState a)
- data LeftoverPatterns = LeftoverPatterns {
  - patternVariables :: IntMap [(Arg Name, PatVarPosition)]
  - asPatterns :: [AsBinding]
  - dotPatterns :: [DotPattern]
  - absurdPatterns :: [AbsurdPattern]
  - typeAnnotations :: [AnnotationPattern]
  - otherPatterns :: [Pattern]
  }
- getLeftoverPatterns :: (PureTCM m, MonadFresh NameId m) => [ProblemEq] -> m LeftoverPatterns
- getUserVariableNames :: Telescope -> IntMap [(Arg 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

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 #
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 #
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 |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term

Methods

applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #

NFData ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ProblemEq -> () Source #
Generic ProblemEq Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq |

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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) |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg (Problem a) = Term

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 :: forall a f. Functor f => ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a) Source #

problemRestPats :: forall a f. Functor f => ([NamedArg Pattern] -> f [NamedArg Pattern]) -> Problem a -> f (Problem a) Source #

problemCont :: forall a f. Functor f => ((LHSState a -> TCM a) -> f (LHSState a -> TCM a)) -> Problem a -> f (Problem a) Source #

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

data AsBinding Source #

Constructors

AsB Name Term (Dom Type) |

#### Instances

Instances details

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 #
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 |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AsBinding = Term

Methods

applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding 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 |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg DotPattern = Term

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 |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AbsurdPattern = Term

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?

- _lhsIndexedSplit :: !Bool

  Have we split on any indexed inductive types?

#### 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 :: forall a f. Functor f => (Telescope -> f Telescope) -> LHSState a -> f (LHSState a) Source #

lhsOutPat :: forall a f. Functor f => ([NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]) -> LHSState a -> f (LHSState a) Source #

lhsProblem :: forall a f. Functor f => (Problem a -> f (Problem a)) -> LHSState a -> f (LHSState a) Source #

lhsTarget :: forall a f. Functor f => (Arg Type -> f (Arg Type)) -> LHSState a -> f (LHSState a) Source #

data LeftoverPatterns Source #

Constructors

LeftoverPatterns |

Fields

- patternVariables :: IntMap [(Arg 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 :: (PureTCM m, MonadFresh NameId 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 [(Arg 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 #