**See the official user manual for the most up-to-date version of the information on this page.**

Anonymous pattern matching functions can be defined using the syntax

\ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }

(where, as usual, `\`

and `->`

can be replaced by `λ`

and `→`

). Internally
this is translated into a function definition of the following form:

.extlam p11 .. p1n = e1 ... .extlam pm1 .. pmn = em

This means that anonymous pattern matching functions are generative.
For instance, `refl`

will not be accepted as an inhabitant of the type

(λ { true → true ; false → false }) ≡ (λ { true → true ; false → false }),

because this is equivalent to `extlam1 ≡ extlam2`

for some distinct
fresh names `extlam1`

and `extlam2`

.

Currently the `where`

and `with`

constructions are not allowed in
(the top-level clauses of) anonymous pattern matching functions.

Examples:

and : Bool → Bool → Bool and = λ { true x → x ; false _ → false } xor : Bool → Bool → Bool xor = λ { true true → false ; false false → false ; _ _ → true } fst : {A : Set} {B : A → Set} → Σ A B → A fst = λ { (a , b) → a } snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p) snd = λ { (a , b) → b }

Page last modified on December 14, 2018, at 06:30 pm

Powered by
PmWiki