Finite map notations

This adds some ad-hoc notations for maps up to size 13, e.g. {[ k1 := a1 ; k2 := a2 ]} for (<[k2 := a2]>{[k1 := a1]}). 13 seems to be enough for many useful cases.

For future reference if notations for larger sets are needed, this is the script I used:

#!/bin/python3

n = 13
# indent by two spaces
indent = "  "


def generate(n):
  # Header
  out = "Notation \"{[ " 

  # notation itself
  for i in range(1, n+1):
    if i > 1:
      out += " ; "
    out += "k" + str(i) + " := a" + str(i)
  out += " ]}\" := \n" 

  # translation of notation
  line = indent + "("
  for i in range(1, n):
    if i > 1:
      line += " $ "
    if len(line) > 70:
      out += line + "\n"
      line = indent + indent 
    line += "<[ k" + str(i) + " := a" + str(i) + " ]>"
  # singleton element
  line += "{[ k" + str(n) + " := a" + str(n) + " ]}"
  line += ")\n" 
  out += line

  out += indent + "(at level 1, format\n"

  # format printing
  line = indent + "\"{[ '[hv' "
  for i in range(1, n+1):
    if i > 1:
      # extra space for printing
      line += " ; ']'  '/' "
    # if len(line) > 70:
      # out += line + "\"\n"
      # line = indent + indent + "\""
    line += "'[' k" + str(i) + "  :=  a" + str(i)
  line += " ']' ']' ]}\")"
  out += line

  out += " : stdpp_scope."
  return out

for i in range(2, n+1):
  print(generate(i))

tests/notation.ref

+test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]}
+     : M (M nat)
+test_3 = 
+{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]}
+     : M (M nat)
+test_4 = 
+{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]}
+     : M (M nat)
+test_op_2 = 
+{[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]}
+     : M (M nat)
+test_op_3 = 
+{[10 := {[20 - 2 := [11]; 1 := [22]]};
+  20 := {[99 + length [1] := [1; 2; 3]]};
+  4 := {[4 := [4]]};
+  5 := {[5 := [5]]}]}
+     : M (M (list nat))
+test_op_4 = 
+{[10 := {[20 - 2 := [11];
+          1 := [22];
+          3 := [23];
+          4 := [1; 2; 3; 4; 5; 6; 7; 8; 9]]};
+  20 := {[99 + length [1] := [1; 2; 3]]};
+  4 := {[4 := [4]]};
+  5 := {[5 := [5]]}]}
+     : M (M (list nat))