coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] "default interpretation"
- Date: Wed, 18 Nov 2015 12:54:52 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f54.google.com
- Ironport-phdr: 9a23:kjL0rBQKI9B4+NDtnlttNuZR8tpsv+yvbD5Q0YIujvd0So/mwa64YB2N2/xhgRfzUJnB7Loc0qyN4/2mBzVLuM7b+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8CVPVwD3WLnKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7oW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKkkCLhsew19zOdJta+GbI9QjOk4L1sUwS5oCgCPj89tmrQj5oj3+pgvBu9qkknkMbva4aPOa8mcw==
I means "this is what the notation will be if you use it right now, without putting any scopes around it"
e.g.,
Locate "*".
(* Notation Scope
"x * y" := Nat.mul x y : nat_scope
(default interpretation)
"x * y" := prod x y : type_scope *)
Set Printing All.
Check _ * _.
(* Nat.mul ?n ?n0
: nat
where
?n : [ |- nat]
?n0 : [ |- nat]
*)
Locate "*".
(* Notation Scope
"x * y" := Nat.mul x y : nat_scope
(default interpretation)
"x * y" := prod x y : type_scope *)
Set Printing All.
Check _ * _.
(* Nat.mul ?n ?n0
: nat
where
?n : [ |- nat]
?n0 : [ |- nat]
*)
On Wed, Nov 18, 2015 at 12:14 PM, Michael Shulman <shulman AT sandiego.edu> wrote:
What does the parenthetical "(default interpretation)" mean when it
occurs in the output of "Locate"?
- [Coq-Club] "default interpretation", Michael Shulman, 11/18/2015
- Re: [Coq-Club] "default interpretation", Jason Gross, 11/18/2015
Archive powered by MHonArc 2.6.18.