Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear MathComp fans,

> Set Printing Universes.
> 
> Require Import mathcomp.ssreflect.ssreflect.
> >From mathcomp Require Import ssrbool ssrfun ssrnat eqtype fintype choice 
> >seq.
> 
> Set Implicit Arguments.
> Unset Strict Implicit.
> 
> 
> (** * Shapes *)
> Definition is_in_shape sh r c := c < nth 0 sh r.
> 
> (** ** A finite type [finType] for coordinate of boxes inside a shape *)
> Section BoxIn.
> 
> Variable sh : seq nat.
> 
> Definition is_box_in_shape b := is_in_shape sh b.1 b.2.
> 
> Structure box_in : predArgType :=
>   BoxIn {coord :> nat * nat; _ : is_box_in_shape coord}.

I should mention that the goal is to show that this sigma-type has a canonical
fintype structure. That's way I put predArgType here and not Set.

The full file is at :

https://github.com/hivert/Coq-Combi/blob/Coq-8.5/theories/Combi/partition.v


Cheers,

Florent