Agda.TypeChecking.Rules.Def

Definitions by pattern matching

checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()

checkAlias :: Type -> Relevance -> Delayed -> DefInfo -> QName -> Expr -> TCM ()

Check a trivial definition of the form f = e

checkFunDef' :: Type -> Relevance -> Delayed -> DefInfo -> QName -> [Clause] -> TCM ()

Type check a definition by pattern matching. The third argument specifies whether the clauses are delayed or not.

trailingImplicits :: Type -> [Clause] -> TCM [Clause]

Ensure that all clauses have the same number of trailing implicits. Example:

  test : Bool → {A B : Set} → Se  test true  {A}     = A
  test false {B = B} = B

trailingImplicits patches these clauses to

  test : Bool → {A B : Set} → Se  test true  {A} {_}     = A
  test false {_} {B = B} = B

such that the arity of the clauses of test is uniform.

dropNonHidden :: Nat -> [Dom (String, Type)] -> [Dom (String, Type)]

dropNonHidden n tel drops n non-hidden domains from tel, including all hidden domains that come before the nth non-hidden one.

splitTrailingImplicits :: Clause -> TCM (Patterns, Patterns)

splitTrailingImplicits c returns the patterns of clause c as pair (ps, ips) where ips are the trailing implicit patterns and ps is the rest.

patchUpTrailingImplicits :: Patterns -> (Patterns, Patterns) -> Clause -> Clause

patchUpTrailingImplicits should (ps, is) c takes a clause c whose patterns are split into (ps, is) where is are the trailing implicit patterns and ps the rest. is has already been patched with omitted implicit patterns (which can occur if named implicit patterns are there originally). should is an extension of is. The returned clause contains an extension of is by new wildcards to match should.

insertPatterns :: [Pattern] -> RHS -> RHS

Insert some patterns in the in with-clauses LHS of the given RHS

data WithFunctionProblem

Constructors

NoWithFunction

WithFunction QName QName Telescope Telescope Telescope [Term] [Type] Type [Arg Pattern] Permutation Permutation [Clause]

checkClause :: Type -> Clause -> TCM Clause

Type check a function clause.

checkWithFunction :: WithFunctionProblem -> TCM ()

checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a

Type check a where clause. The first argument is the number of variables bound in the left hand side.

containsAbsurdPattern :: Pattern -> Bool

Check if a pattern contains an absurd pattern. For instance, suc ()

actualConstructor :: QName -> TCM QName