The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

> From: "Lukasz Stafiniak" 
> <l_stafiniak AT hoga.pl>
> To: 
> <coq-club AT pauillac.inria.fr>
> Date: Wed, 20 Aug 2003 21:33:40 +0200
> Subject: [Coq-Club] Tactic Language suggestions
> 
> Hi,
> 
> Is the Ltac language going to be enlarged?
> If so, I have some suggestions:
> 
>  - identifiers generation: concatenating two identifiers
>    to get a new identifier; generating a
>    fresh (free) identifier from given one by adding
>    a numeric postfix
> 
>  - accessing the type of a term (e.g. hypothesis identifier),
>    by a construct "Match Typeof t With"
> 

The like of "Match Typeof t With " is already provided in Ltac, using
a construct with the following form:


Let v = Check t In Match v With

Here is an example:

bahia$ ledit /usr/local/coq-7.4/bin/coqtop
Welcome to Coq 7.4 (Feb 2003)

Coq < Goal O=O -> (S (S O))=(S (S O)).
Intros H.
1 subgoal
  
  ============================
   (0)=(0)->(2)=(2)

Unnamed_thm < 1 subgoal
  
  H : (0)=(0)
  ============================
   (2)=(2)

Unnamed_thm < Let v = Check H In Match v With [ ?1 = ? ] -> Cut (S ?1)=(S ?1).
2 subgoals
  
  H : (0)=(0)
  ============================
   (1)=(1)->(2)=(2)

subgoal 2 is:
 (1)=(1)


  Yves

Yves.Bertot AT inria.fr
  Tel: (+33/0)4 92 38 77 39  Fax: (+33/0)4 92 38 50 60
INRIA Sophia-Antipolis 2004, route des lucioles, B.P. 93,
06902 Sophia Antipolis Cedex (France).
http://www.inria.fr/lemme/Yves.Bertot