Skip to main content
Proof Assistants Beta

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

6
  • $\begingroup$ I suppose the last two paragraphs, together with the pseudo-syntax of the question, lead one towards having with-abstraction expressions (like the generalize tactic, IIRC, in Coq). $\endgroup$
    – James Wood
    Commented Feb 29 at 15:21
  • $\begingroup$ Thanks! Cockx's talk is close to answering what I want to know. If I understand correctly, he's trying to introduce a version of well-scoped syntax that permits (among other things) modifying the scope by replacing x with new variables, for the purpose of a correct-by-construction implementation of core Agda. What he comes up with is interesting but doesn't quite do what he wants. But I would be content to know what Agda currently does! What sort of variables and contexts does it use that allow replacing x with new variables? $\endgroup$
    – Mike Shulman
    Commented Feb 29 at 17:59
  • $\begingroup$ Heads up that I added a bit more to the question. In particular, it seems to me that in the presence of indexed datatypes, it isn't sufficient to just insert the all the new variables in any one place in the context. $\endgroup$
    – Mike Shulman
    Commented Mar 1 at 7:00
  • $\begingroup$ You are right, things are hairier with indices. I think there is no easy solution there, you need to manipulate whole contexts and rely on a form of unification. The relevant reference is probably Jesper Cockx's PhD thesis. Skimming through, on p. 44 he gives a high level condition for the context in which each branch lives, which cannot be simply described from the one of the whole pattern-matching. Then a large part of the thesis is concerned with how to construct contexts (and case-trees) satisfying the criterion and being well-behaved. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Mar 1 at 12:29
  • $\begingroup$ Thanks. It looks to me like p44 is defining a substitution to be used when evaluating a pattern-matching definition. My question is about what the codomain context of this substitution is. This seems like it ought to be somewhere in section 2.2 about type-checking, but on a first skim I cannot find where he specifies how to reorder the context. $\endgroup$
    – Mike Shulman
    Commented Mar 1 at 18:05