ssreflect - [ssreflect] a new question about bigop (for Sophie...)

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] a new question about bigop (for Sophie...)

From: Laurence Rideau <>
To:
Subject: [ssreflect] a new question about bigop (for Sophie...)
Date: Wed, 18 Jun 2014 15:43:28 +0200

We are trying to use bigop for the max operator.
The question is :
why are the properties proved on finite types (and not on sequences)?

thanks
laurence & sophie.

[ssreflect] a new question about bigop (for Sophie...), Laurence Rideau, 06/18/2014
- RE: [ssreflect] a new question about bigop (for Sophie...), Georges Gonthier, 06/19/2014

List archive

[ssreflect] a new question about bigop (for Sophie...)