Commit d7d7b30b authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Define record update notation at level 10

parent a87332ee
Pipeline #10598 failed with stage
in 1 minute and 27 seconds
......@@ -90,8 +90,8 @@ Hint Extern 1 (Setter _) => SetInstance_t : typeclass_instances.
Module RecordSetNotations.
Delimit Scope record_set with rs.
Open Scope rs.
Notation "x [[ proj := v ]]" := (set proj (constructor v) x)
(at level 12, left associativity) : record_set.
Notation "x [[ proj ::= f ]]" := (set proj f x)
(at level 12, f at next level, left associativity) : record_set.
Notation "x [ proj := v ]" := (set proj (constructor v) x)
(at level 10, left associativity) : record_set.
Notation "x [ proj ::= f ]" := (set proj f x)
(at level 10, f at next level, left associativity) : record_set.
End RecordSetNotations.
Supports Markdown
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