From p. 3 of the paper "Why Dependent Types Matter": "We have given a complete program, but Epigram can also typecheck and evaluate incomplete programs with un

From p. 3 of the paper "Why Dependent Types Matter": "We have given a complete program, but Epigram can also typecheck and evaluate incomplete programs with unfinished sections sitting in sheds, [···], where the typechecker is forbidden to tread. Programs can be developed interactively, with the machine showing the available context and the required type, wherever the cursor may be. Moreover, it is Epigram which generates the left-hand sides of programs from type information, each time a problem is simplified with ⇐ on the right."