coq-community/corn

Notation Clash

Closed this issue · 5 comments

rnrand commented

The file CLogic.v defines the following two notations:

Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
  (at level 0, x at level 99) : type_scope.
Notation "{ x : A  |  P  |  Q }" :=
  (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
  type_scope.

However the Coq standard library (at least as of 8.5) has the following notations:

Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
  type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
  type_scope.

The first notation clashes with CLogic's notation, the last two notations seem to express what the CLogic notation intends.

This is breaking developments that depend on CoRN, for instance the quantum computing library here: https://www.dropbox.com/sh/fhldyg1mfnxdmcl/AAAvQZz1i1mjdL5TKzwcWwyva/CoRN?dl=0

spitters commented
spitters commented

I've updated again. Hoping it is better now.
One problem is that the quantum guys never made a proper release, or contributed code to the main branch.
Their README says they are still depending on v8.4, which we don't support.

rnrand commented

Did you commit something new to the repository?

Also, it sounds like the quantum guys are in the process of moving over to MathComponents. I still might try to modify their current code to get it working with C-Corn.

spitters commented

The corn library compiles with 8.5. I am not sure what the quantum guys have been doing.
I guess we should ask @jaapb .

spitters commented

Closing this, as we are now following master,