(version: 1.1.2)

18 Beta-reduce mode

Beta-reduce mode is a "beta-reduction explorer". There are three ways to enter beta-reduce mode:

1. C-i b Enter beta-reduce mode with a prompted expression. Copies global scope and local scope if a span is selected.
2. C-i B Enter beta-reduce mode with the selected span and its scope
3. C-i t Enter beta-reduce mode with the selected span’s expected type and its scope

19 Controls

C-i n

Replace the selected span with its normalization

C-i h

Replace the selected span with its head-normalization

C-i u

Perform a single reduction on the selected span

C-i =

Replace the selected span with a prompted expression, if convertible

C-i r

Synthesize an equational type from a prompted expression and rewrite the selected span using it

C-i R

Same as “C-i r”, but beta-reduces the selected span as it looks for matches

C-i p

Reconstruct a proof from each step taken so far

C-i ,

Undo

C-i .

Redo