coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gert Smolka <smolka AT ps.uni-saarland.de>
- To: "coq-club AT inria.fr Club" <coq-club AT inria.fr>
- Subject: [Coq-Club] Notation Command
- Date: Thu, 14 Feb 2019 15:54:09 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=smolka AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=smolka AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
- Ironport-phdr: 9a23:sez28R9yMBQJof9uRHKM819IXTAuvvDOBiVQ1KB41ewcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/0hykIODE37WLZhMJugqxcux+huwV/w4vIbIGVKPZyYKXQds4aS2pbWcZRUjRMDIKiYIsVE+oKIPtWr4z6p1sKrhuxHxSnCeT0yj9NgX/22a463P46HAHexwwsBc8OsHLVrNnsL6cdS/q6zLPMzTrZafNZxC3x55XWfR04p/yHQLF+cdLJxEUyGQ7IgU+cpIjkMj+P1OkBqXaX4up4We+rhWMrsRx9rzysy8s2lIXEiZ4ZxkrG+Ch4xos+OMe2R1RhYdG+FZtdryGaOJVyQsMlW2xopDw6yrwauZ68eigG0o4nxh/FZ/yadYiI4wvvVP2LLjhinnJlfKiwhxCv/kS61+LzSNG40FdMriVbjtnBrm0B2hLc58SdTvZw/12t1DSV2wzN6uxIOUU0mrDaK54lzL4wjJ0TsUHbEy/tnUX2i6uWdkY+9eWz8+Tnea/qpoKaN491kw3+Kb4hldalAeQ8KAcOWXWU9f6h27L95UH5WqlFjuUqkqnFt5DXPdgUpqmgAwNMzokj7wu/ACy93dQDnXgHKUpFdwidg4joPVHOOvH4Au2lj1Siijc4j8zBa/fqBYyIJXzemp/ge6x84ghS0kIYyc1VrdoAAbYYZfn3R0XZtdrCDxZ/PRbikMj9D9Ao+Y4ERSq0B6idM6qa5USN4eYsKsGUf8kIvje4MPEs/frni3N/lVJLLvrh5ocedH3tRqcuGE6ee3e52o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdmvmMjE8S7C4aGXYmkmriI2iv9EpAEPzkaWGDJKm/hcsC/Y9lJcDibeJcziidCSL6gDpQo3AuqvQn2jbZqfLKNp38o8Kn73d0w3NX90BE/8TsuUJaByWCRSGcyhHFOWjk3mbt2qFZ5w1GPl6R10aRV
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
Archive powered by MHonArc 2.6.18.