coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Difference between uconstr and open_constr
- Date: Tue, 26 Jul 2016 18:31:36 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
- Ironport-phdr: 9a23:g7lSiRUH4LjYC2/xNG3lSLX4NjXV8LGtZVwlr6E/grcLSJyIuqrYZheEt8tkgFKBZ4jH8fUM07OQ6PG4HzJcqs7R+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0pcGYO1UArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7axHwaW3kWmxwAJwXE8hz8Qt+lsCz8t+lw3CSXFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==
On 07/26/2016 06:23 PM, Robbert Krebbers wrote:
Dear Coq club,
Could someone explain me the difference between the tactic argument types uconstr and open_constr?
Thanks,
Robbert
The differences are (I may be forgetting some):
1. uconstrs are not type-checked until converted to something else (constr, open_constr) or until type_term is called on them. Hence it is possible to construct uconstrs that can't possibly type check:
Goal True.
let X := uconstr:(I I I) in idtac X.
But, one can save time by not type-checking while constructing complex uconstrs.
2. the holes in uconstrs do not become subgoals until the above type checking occurs, while the holes in open_constrs become subgoals immediately (as the type checking on open_constrs occurs immediately).
3. there is a "uconstr:(..)" form for Ltac, but no corresponding one for open_constr (although one can somewhat get around this via a Tactic Notation).
-- Jonathan
- [Coq-Club] Difference between uconstr and open_constr, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
- [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
- [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Pierre-Marie Pédrot, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
Archive powered by MHonArc 2.6.18.