Ssreflect Users Discussion List

[Georges Gonthier <>]

Indeed, this is an old problem, which is not due to the ssreflect plugin per 
se, but to the ssreflect.v vernacular file, which creates a keyword for the 
'of' token.
Amazingly, 'of' is an ordinary identifier in the Coq grammar. The ssreflect 
plugin code anticipates this change and does unspeakable things to the Coq 
parser so that this does not break the tactic syntax which, due to 
limitations in the original design of  the camlp4 parser generator (fixed in 
camlp5 but not in its evil camlp4 twin), cannot be programmed to accept the 
'of' keyword when it expects the 'of' identifier.
   Unfortunately the let .. := type of is a recent addition to Ltac, which 
was not included in the compatibility code. If I may say so, it is a dubious 
addition, because this sort of thing is easily (and more fruitfully) done in 
Gallina than in Ltac. With the ssreflect extension you can simply define
   Definition typeOf {T} & T := T.
then write, say
  Lemma foo x : x = true.
  set B := typeOf x. (* B := typeOf x in context *)
  unfold typeOf in B. (* B := bool in context *)
If you want to be fancier you can add an
   Arguments typeOf {T} / _.
declaration to use simpl instead of unfold in the third line, or even a 
Notation hiding an explicit beta redex
  Notation typeOf c := ((fun T & T => T) _ c).
which would let you use lazy beta instead of simpl, though this would 
probably never be necessarily as Coq reduces beta redexes greedily.
Note also that ssreflect.v provides several related though somewhat more 
complex definitions (argumentType, and co.).

Georges

-----Original Message-----
From: Laurent Théry [] 
Sent: 04 September 2013 10:29
To: t x
Cc: 
Subject: Re: Obtaining Type of a Term

On 09/04/2013 03:37 AM, t x wrote:
> Hi,
>
>   Here is my minimal failure case:
>
> https://gist.github.com/anonymous/35b90fd523ace14dffd3
>
>   The code executes fine (with "move =>" replaced with "intros") in 
> plain Coq.
>
>   However, in ssreflect, I get an error
>
>   "Syntax error: 'with' or 'in' ..." on line 10
>
>   How do I rewrite this in ssreflect? (in particular, I want to 
> extract the type of a term).
>
> Thanks!

It seems that ssreflect has broken the way "type of" is parsed in Ltac. 
A quick fix is to rename "type of" before loading ssreflect.

Require Import ZArith String.
Ltac typeOf x := type of x.
Require Import ssreflect eqtype.

Lemma lem:
forall (a b: nat)
(H: {a = b } + {a <> b}), False.
Proof.
move => a b H.
let t := typeOf H in
set (x := t).