ssreflect - set and pattern

Subject: Ssreflect Users Discussion List

List archive

set and pattern

From: Laurent Thery <>
Cc: ssreflect <>
Subject: set and pattern
Date: Thu, 26 May 2011 10:40:49 +0200 (CEST)

Hi,

I often use set to name a subterm of my goal,

For example,

set u := (_ = _)

to name my first equality.

Is it possible to use the new pattern of ssreflect 1.3 in combination with
set?
Something like that
set u := X in _ = X.
to name the first subterm at the right hand of an equality.

--
Laurent

basic question about matrices, Vincent Siles, 05/19/2011
- Re: basic question about matrices, Laurent Théry, 05/19/2011
  - Re: basic question about matrices, Vincent Siles, 05/19/2011
    - Re: basic question about matrices, Laurent Théry, 05/19/2011
      - Re: basic question about matrices, Vincent Siles, 05/19/2011
        
        Re: basic question about matrices, Vincent Siles, 05/19/2011
        
        set and pattern, Laurent Thery, 05/26/2011
        
        RE: set and pattern, Georges Gonthier, 05/26/2011
        
        Re: set and pattern, Enrico Tassi, 05/26/2011
- RE: basic question about matrices, Georges Gonthier, 05/19/2011
  - Re: basic question about matrices, Vincent Siles, 05/19/2011
    - RE: basic question about matrices, Georges Gonthier, 05/19/2011

List archive

set and pattern