(version: development)

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 selection and its scope
3. “C-i t” Enter beta-reduce mode with selection’s type/expected type and its scope

19 Controls

f/b/n/p/...

Regular cedille-mode syntax navigation

C-i n

Replace selection with its normal form

C-i h

Replace selection with its head normal form

C-i u

Only reduce selection by one step, then stop

C-i =

Replace selection with some other expression (prompt), if βη-equal

C-i r

Rewrite selection with a proof of some equation

C-i R

If “C-i r” operates like a ρ term, this is like a ρ+ term: it β-reduces as it looks for matches

C-i f

Fill this type with some term (prompt), if it type-checks

C-i a

Abstract the outermost binder (λ/∀/Π/➔/➾) of the entire expression

C-i c

Case split upon some term (prompt), spawning another buffer for each case

C-i p

Reconstruct a proof of your work from each step taken so far

C-i ,

Undo

C-i .

Redo