The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Thank you!

As I have Coq on Windows for now, I will simply wait for new version.

 

My current workaround is such:
 

Require Import Utf8 List.
Set Implicit Arguments. 

 

Fixpoint list_as_pred T (L: list T): T → Prop :=
  λ a, match L with
  | nil => False
  | x :: nil => a = x
  | x :: t => a = x ∨ list_as_pred t a
  end.
Notation "{ x , .. , z }" := (list_as_pred (cons x .. (cons z nil) .. )). 

 

Definition empty_set {T} := λ (x: T), False.
Notation "{ }" := empty_set. 

  

Definition X := {1}. Print X.

Definition Y := {1, 2}. Print Y.

Definition Z: nat → Prop := {}. Print Z.

 
Maybe it's useful someone else who tinkers with naive set theory.

On Mon, Sep 12, 2016 at 6:30 PM, Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

You actually made nothing wrong. This is a bug, with a short fix at [1]
if ever you'd like to recompile Coq with it.

I don't see an immediate workaround, except binding also "a" in the
recursive notation, or expanding the recursive notation into a
collection of finite instances of it.

Best,

Hugo Herbelin

[1] https://github.com/coq/coq/commit/90e5945e1666540bc18e7a9b831d136041f4e487

On Mon, Sep 12, 2016 at 05:13:55PM +0300, Ilmārs Cīrulis wrote:
> Hello,
>
> I made a notation and tested it. It was parsed correctly, but it wasn't
> display.
> Where is my mistake?
>
>
>     Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) ..
>     (a = v))): set_scope.
>     Open Scope set_scope.
>     Check ({1, 2}).
>
>
> The "check" command displays
>
>     fun a : nat => a = 1 \/ a = 2
>          : nat -> Prop
>
> while I would like to see something like this:
>
>     {1, 2}:  nat -> Prop
>
>
>
> Thank you!
>
>
>