Skip to content
Snippets Groups Projects
Commit b2c5f1fe authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'map-notations' into 'master' 

Fix finite map notations for Coq < 8.13

See merge request !237
parents 37a080d1 2941aae4
No related branches found
No related tags found
1 merge request!237Fix finite map notations for Coq < 8.13
Pipeline #43747 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 26 additions and 23 deletions
theories/base.v
+ 26
− 23
View file @ b2c5f1fe
......@@ -1053,64 +1053,67 @@ Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
recursive notation system, so we define individual notations
for some cases relevant in practice. *)
(* The "format" makes sure that linebreaks are placed after the separating semicola [;] when printing. *)
(* TODO : we are using parantheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
and earlier have trouble with using the notation for printing otherwise.
Once support for Coq 8.12 is dropped, this can be replaced with [$]. *)
Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
(<[ k1 := a1 ]>{[ k2 := a2 ]})
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]>{[ k3 := a3 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]>{[ k3 := a3 ]}))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]>{[ k4 := a4 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]>{[ k4 := a4 ]})))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]>{[ k5 := a5 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]>{[ k5 := a5 ]}))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]>{[ k6 := a6 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]>{[ k6 := a6 ]})))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]>{[ k7 := a7 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]>{[ k7 := a7 ]}))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]>{[ k8 := a8 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]>{[ k8 := a8 ]})))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]>{[ k9 := a9 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]>{[ k9 := a9 ]}))))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
<[ k9 := a9 ]>{[ k10 := a10 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
<[ k9 := a9 ]>{[ k10 := a10 ]})))))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
<[ k9 := a9 ]> $ <[ k10 := a10 ]>{[ k11 := a11 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
<[ k9 := a9 ]> ( <[ k10 := a10 ]>{[ k11 := a11 ]}))))))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ; ']' '/' '[' k11 := a11 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
<[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]>{[ k12 := a12 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
<[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]>{[ k12 := a12 ]})))))))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ; ']' '/' '[' k11 := a11 ; ']' '/' '[' k12 := a12 ']' ']' ]}") : stdpp_scope.
Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ; k13 := a13 ]}" :=
(<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
<[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
<[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]> $ <[ k12 := a12 ]>{[ k13 := a13 ]})
(<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
<[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
<[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]> ( <[ k12 := a12 ]>{[ k13 := a13 ]}))))))))))))
(at level 1, format
"{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ; ']' '/' '[' k11 := a11 ; ']' '/' '[' k12 := a12 ; ']' '/' '[' k13 := a13 ']' ']' ]}") : stdpp_scope.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment