The Coq mailing list

[Perce Strop <percestrop AT outlook.com>]

Hi,

You can put your notation inside a module inside the module and then only import the inner module but not the rest of the module. Maybe the idea is clearer with actual code.

  Require Import NArith.

  Delimit Scope ord_scope with ord.

  Module Type OrderedType.
     Axiom S: Set.
     Axiom lt: S -> S -> Prop.
     Axiom lt_trans: forall i j k: S, lt i j -> lt j k -> lt i k.
  End OrderedType.

  Module OrderedTypeFacts (M: OrderedType).

     Definition gt (i j: M.S) := M.lt j i.

  Module Notation.

     Notation "i < j" := (M.lt i j): ord_scope.
     Notation "i > j" := (gt i j): ord_scope.

  End Notation.
  Import Notation.
  
  (* Here my axiom is fine, no probs using the notation *)
  Axiom int32_lt_to_gt:
     forall i j: M.S,
     (i < j)%ord ->
     (j > i)%ord.

  End OrderedTypeFacts.

  Definition int32: Set
  := { n: N | (n < 2^32)%N }.

  Inductive int32_lt: int32 -> int32 -> Prop
  := mk_int32_lt:
        forall i j: N,
        forall H1: (i < 2^32)%N,
        forall H2: (j < 2^32)%N,
        (i < j)%N ->
        int32_lt (exist _ i H1) (exist _ j H2).

  Theorem int32_lt_trans:
     forall i j k: int32,
     int32_lt i j ->
     int32_lt j k ->
     int32_lt i k.
  Proof.
  intros [i H1] [j H2] [k H3] H4 H5.
  inversion H4 as [l m H6 H7 H8 H9 H10].
  inversion H5 as [n p H11 H12 H13 H14 H15].
  apply mk_int32_lt.
  apply Nlt_trans with (m := j); assumption.
  Qed.

  Module int32_OrderedType <: OrderedType.
     Definition S := int32.
     Definition lt := int32_lt.
     Definition lt_trans := int32_lt_trans.
  End int32_OrderedType.

  Module int32 := OrderedTypeFacts int32_OrderedType.

  Import int32.Notation.

  Axiom int32_lt_to_gt:
     forall i j: int32,
     (i < j)%ord ->
     (j > i)%ord.

Perce