The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Dear Vladimir,
  Laurent Chicli did something like that in this in his thesis, as an 
ocaml patch to the
version of coq at that time; it was called "fAssert".
---Carlos


On 01/07/2014 09:51 PM, Vladimir Voevodsky wrote:
> Is there a reason why Coq's proof engine does not accept a possibility of 
> dependent goals? For example if I need to provide an object of an inductive 
> type
>
> Inductive I := Iconstr :  forall ( x0 : T0 ) ( x1 : T1 ) , I .
>
> where T1 in general depends on x0, I would like to say "apply Iconstr."  and 
> get provided first with the goal to fill in x0 in T0 and then with the goal to fill in 
> x1 in the appropriately substituted T1.
>
> This should not be too hard to implement and it would make many proofs easier.
>
> Vladimir.


--


------ ------ ------ ------ ------ ------ ------ ------ ------ ------

Carlos T. Simpson
C.N.R.S., Laboratoire J. A. Dieudonne, Universite de Nice-Sophia Antipolis

"Homotopy Theory of Higher Categories" now published!

Cambridge University Press, October 2011

http://www.cambridge.org/gb/knowledge/isbn/item6172978/

------ ------ ------ ------ ------ ------ ------ ------ ------ ------