People who code: we want your input. Take the Survey

# Tag Info

7

A subterm of a closed term is not necessarily a closed term. A calculus of closed terms would have to model open terms as well anyway. Pretty much any definition on terms relies on induction over the structure of the terms, and to define something for closed terms of the form $\lambda x. M$, you need to define that thing for the open term $M$. There are ...

2

For examples like this, they can often by easily written interactively just looking for the only thing possible to do at each stage. So for instance, you start with: wp e = ? and the only option is to apply e, at which point Agda will tell you you need to provide $((A → B) → A) → A$, so you introduce a lambda: wp e = e (λ k -> ?) Now you need to give an ...

Top 50 recent answers are included