case package:Agda

Branches in a case tree.

Case n bs stands for a match on the n-th argument (counting from zero) with bs as the case branches. If the n-th argument is a projection, we have only conBranches with arity 0.

Is this a match on an erased argument?

Monadic version of either with a different argument ordering.

Case distinction for lists, with list first. O(1). Cf. ifNull.

Case distinction for lists, with list first. O(1). Cf. ifNull.

Case distinction over lazy list.

Version of maybe with different argument ordering. Often, we want to case on a Maybe, do something interesting in the Just case, but only a default action in the Nothing case. Then, the argument ordering of caseMaybe is preferable.

caseMaybe m d f = flip (maybe d) m f

Monadic version of caseMaybe. That is, maybeM with a different argument ordering.

Version of maybe with different argument ordering. Often, we want to case on a Maybe, do something interesting in the Just case, but only a default action in the Nothing case. Then, the argument ordering of caseMaybe is preferable.

caseMaybe m err f = flip (maybe err) m f

Produced by an interactive case split.

Do case analysis on a term. CaseDT is scoped in the same way as fast case trees for the abstract machine: When matching actually succeeds, the variable that was matched gets replaced by its arguments directly in the context.

Failure of the makeCase interactive tactic.