Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Difference between uconstr and open_constr

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Difference between uconstr and open_constr


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page