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))