Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Definitions by pattern matching

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

Check a trivial definition of the form f = e

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

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

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

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)]Source

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)Source

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 -> ClauseSource

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 -> RHSSource

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

checkClause :: Type -> Clause -> TCM ClauseSource

Type check a function clause.

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

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

containsAbsurdPattern :: Pattern -> BoolSource

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