Hi, > Isn't elaborating a shed with a call to an undefined function (e.g. at > the top) the same as stating a programming problem? The required return > type follows from the context, the hypothesis follows from arguments and > their types and you've just given a call pattern.
Precisely, but we beleive that this is another of the jobs of the 'where' clause, a call to an undefined function should create a local programming problem, with hyps and goal filled in for you and access to the context of the parent. It's non trivial how then to lift the local function to a global one, some hypotheses from the parent would need to be abstracted for starters and you would probably want some generalisation to happen to make the new global function more useful. The global guy will form part of a future story about refactoring Epigram programs. Peter
