The Coq mailing list

[Nico <nlehmann AT dcc.uchile.cl>]

Well I think you are right.

What I was expecting is the posibility for a tactic to be defined inside a module preserving the encapsulation but I see that this is not possible.

Thanks.

On Mon, May 18, 2015 at 9:48 PM Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

Hi, Nico --

Perhaps I misunderstand what you are looking for, but here is an example.

Axiom HiddenType : nat -> Type. (* the natural number should only be 0 *)

Axiom it : forall x, HiddenType n.  (* n should only be even *)

Definition using_hidden : HiddenType 0 := @it 0.

Definition bad : HiddenType 1.

let x := eval red in using_hidden in

match x with

  | ?X ?Y => exact (X 1)

end.

Defined.

In the example [using_hidden] is meant to be generated via the tactic that you propose. Here, the definition of [bad] avoids using the tactic to construct any a value of type [HiddenType 1]. There is no way in the Coq system to circumvent this.

On Mon, May 18, 2015 at 6:05 AM, Nico <nlehmann AT dcc.uchile.cl> wrote:

On Fri, May 15, 2015 at 3:40 PM Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

Hi, Nico --

I don't believe this is possible. If the type is embedded inside of a term, then that term could be opened up via Ltac, and then Ltac could construct a term using constr and avoid your check.

I don't clearly understand what do you mean here.

 

It is possible to express your restriction via arguments? For example, if you want a type function that requires a type with a decidable equality there are several ways to do it:

I don't think is posible to express the restricion in this way because I need to access the axioms that an argument take as assumptions.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/