Coq glossary

βι normal form

A term is in βι normal form if it cannot be reduced further by simplifying application of lambdas (i.e. terms of the form (fun x => …) … — this is β reduction), nor match forms on explicit constructors (this is ι reduction). For example, the following term is not in βι normal form, since it contains a match on an explicit pair:

match (1, 2) with | (x, y) => id (x + y) end

One step of ι reduction, followed by one step of β reduction, yields a normalized term:

Eval cbv iota in match (1, 2) with                  | (x, y) => id (x + y)                  end.

= (fun x y : nat => id (x + y)) 1 2 : nat

Eval cbv beta in (fun x y: nat => id (x + y)) 1 2.

= id (1 + 2) : nat