Ecce Commands

Remember, press return twice!

Management

  • {}  quits

New Entries

You can make new stuff appear just behind the turnstile like this:

  • x :S  declares a parameter x of type S
  • x => s:S  makes a definition, that x has value s of type S
  • x => ? :S  makes a hole x of type S

Navigation

You can shuffle up and down the context like this:

  • <-  moves up one entry
  • <-x  moves up to just before the most recent x
  • <-x^n  skips over n xs and moves to just in front of the one before that
  • ->  moves down one entry, with the same variations

At the moment, the best way to go to top or bottom is to try to go to something which doesn’t exist, incurring the message Bump! but otherwise achieving the desired effect. Doubtless, we shall rectify this at some stage.

Editing Entries

If the turnstile is sitting just before an entry, you may adjust its status in these ways:

  • => s  fills a hole, replacing ? by s if s has the hole’s type
  • => ?  revokes a definition, replacing the indicated value by a ?
  • \|/   deletes an entry entirely

Ecce propagates the consequences of these actions through the context. This makes the ‘undo’ operations quite dangerous: an entry whose type no longer makes sense also gets deleted; a definition whose type is still ok but whose value is broken gets revoked. It’s a rather subtle operation, because a definition can remain a definition without retaining the same value. Here’s an example, cut and pasted from an actual session


--------------------------------------------------------
X : *
F : all x : X => *
c : X
C : F c
|-
x => c : X : X
y => x : X : X
z => C : F y : F y
--------------------------------------------------------
[Ecce] => ?
[Ecce]
--------------------------------------------------------
X : *
F : all x : X => *
c : X
C : F c
|-
x => ? : X
y => x : X : X
z => ? : F y
--------------------------------------------------------

See? Even though y => x survives, z breaks because y means less than it did before. We say that y has been degraded: revoking is just one way of degrading.

Running Things

  • (t)  typechecks and evaluates t given what’s in scope at the turnstile, printing the resulting value and type

Leave a Reply