coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Notation Command

From: Li-yao Xia <lysxia AT gmail.com>
To: Gert Smolka <smolka AT ps.uni-saarland.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Notation Command
Date: Thu, 14 Feb 2019 10:03:39 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f177.google.com
Ironport-phdr: 9a23:pDPCTRzPUY4HonnXCy+O+j09IxM/srCxBDY+r6Qd2+sSIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CWGRPQMhRWSxCDI2yYYQAAOgOMvpXoYTmu1sDrwGzCRWwCO7hyDJFgGL9060g0+QmFAHLxAouH9MXvHXUttr1M7oZXuG0zKbS0D7OaPdW2Dfm6InHcxAuu+qBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvWuD7+d4S+6jl2oqpxtyrzWv3MsglJfFipwPxlzZ9yh0wp45KcO5RUJnY9OpFZVQui6YOodqR84vQmRltSkmxrEat562eTQFx44pxxPdbvGKfYaF4hztVOuULzd3mm5qd6i6ihmp80Wv0enxW8+p21hQtCVFiMPDtnUV2hzT9MeHTvx981+k2TmV1gDT7vhIIVk3labGMpIhzKM8m5gRvEjZES/2n0L2jKCSdko64OSn9+PnYrD+qp+dMY97lB3+P7wwlsCjBek0KAsDUmiB9eiiyrHv41f1TKhIg/A0iqXZtYrVJcUfpq63GQ9V1YMj5g67Dzamy9QZkngHI0hedRKIiojmIVDOIPTiAfijhFSslS9nx+raMb35HpXNMn/Dna/9crZ68k5Q0RY8zdRC551PEbwBO/LyWkrptNPCFBM5Mgq0w/zmCNpnzI8eV3iPUeelN/b9vEWUrtkqJO2PbcdBozP6L/ssz+b1y2I/mBoGdKCz2ZIRZDa0E6I1DV+eZC/Ig5IQGGBCjgs3BLjumUaSUDd7aHO7XqZ67TY+XtH1RbzfT5yg1eTSlBywGYdbMyUfUgjVQCXYMr6cUvJJUxq8Z8pokzgKT7+kEtZz2hSntQu8wL1ifLONpn8o8Kn73d0w3NX90Ako/GUtXcuY2mCJCWpzmzFQHmJk7OVEuUV4j2y7/+14jvhfT4IB4vpIVkIjNseZwbUlVJb9XQXOetrPQ1GjEI2r

Hi Gert,

Try this:

Notation D k x := (x%nat = (x / k) * k).

Coq needs to decide what scopes to use to parse the arguments of D, but the original definition of that notation makes that choice ambiguous. Opening scopes using %nat resolves the ambiguity.

Li-yao

On 2/14/19 9:54 AM, Gert Smolka wrote:

The following notation commands are both rejected. How can I fix this? Gert

From Coq Require Import Arith.
Fail Notation D k x := (x = (x / k) * k).
Fail Notation "'D' k x" := (x = (x / k) * k) (at level 70).
(* x is here used in scope nat_scope while it was elsewhere used in the empty
scope stack *)

[Coq-Club] Notation Command, Gert Smolka, 02/14/2019
- Re: [Coq-Club] Notation Command, Li-yao Xia, 02/14/2019