coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Using many interpretation scopes

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Using many interpretation scopes
Date: Mon, 29 Jul 2019 10:00:20 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg1-f171.google.com
Ironport-phdr: 9a23:hRuTgRXxWbyI0XeB/PdgScmYTl7V8LGtZVwlr6E/grcLSJyIuqrYbBOBt8tkgFKBZ4jH8fUM07OQ7/m6Hz1YqsbZ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLssQanYRuJ6UtxhDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuBKvqQJizYHaeoGbOvlwcazBct4BWWpNQtxcWzBdDo6mc4cCCfcKM+ZCr4n6olsDtRWyCxG2COjy1jFHnHD23a0g3OQ/Dw7G2hEvH8gUv3jasd74M6ESUOCvzKbSwjXDb+5W1Sn/5YTVfB0tv+qBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvWac7+plT+2vimgnphlxoji1x8cgkJPJiZwOylze9CV5xp45JcemR05ne96kF4dQuD+VNotqWcMuWWdotzgmyrAApJW1fzAKxYw5yxLDb/GLaYuF7xL5WOqPPDt1hGhpdK+9ihqv6USs1+LxWtOp3FtEqidJiNnBu3QX2xDO5cWLVv1w9Vq71zmVzQDc8ORELFg0laXFL54hxaY9lp8JvkTCGi/6gV32jKCLekk99Oik9ubqbqj8qp+TMI90jQ7+MqAwlcClHes4NQ0OU3Ca+eS6yrLj4VX0TKtWgvAyiKXUs5DXKd4FqqKkAwJZyJsv5hSiAzu+1dQXh3gHLFZLeBKdiIjpPknDIPb4DPelmVusnzdrx+3YMrDjH5nAIGbPnazufbZ48UFcyQ4zwcpD6JJTD7ENOOjzVVPptNzEEh85NBS5zPrgCNVkz48RRWaPArKCP67Jql+J5ucvI/GWa4MPuTb9LeIl5//0gnMjl18dZ/rh4ZxCY3ehW/9iPk+xYHz2g95HH31ZhAcmSP3WjwjId3gbXX+9X6si6zc3EovsRdPFV5qkj7ychnjiRcd+aWVPC1TKGnDtIdaqQfAJPWi0ZIdbmzMEXKasTYM73Fvm4Anr0bNoLveOpXRD77rs0dF046vYkhRkpm88NNiUz2zYFzI8pWgPXTJjhPku83w48U+K1O1Du9IdENVS4/1TVQJjbMzTyuV7D5b5XQeTJ47UGmbjec2vBHQKdvx0w9IKZBwjSdCrjxSGxyXzRrFMyOXNC5sz/abRmXP2IpQlkiqU5Owal1AjB/B3Gyi+nKcmrlrcAofIlwOSkKP4Lak=

I find that it is convenient to use many interpretation scopes for
notations, so that I can use the same symbol in different scopes with
different meanings, without overriding notations. Is there any
performance overhead with many open scopes? Is using many scopes
deprecated for this, or for reasons of style?

Thanks and regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Using many interpretation scopes, N. Raghavendra, 07/29/2019