"atomic" branch

Atomic

The atomic branch adds a family of reduction tactics which apply a single of reduction at a certain position in a term.

Reduction tactics

• atomic fun: function application (beta reduction)
• atomic fix: fixpoint expansion
• atomic cofix: cofixpoint expansion
• atomic match: match reduction
• atomic let: let-in reduction (zeta reduction)
• atomic unfold: definition expansion (delta reduction)

TODO

• support all reductions
• make accessible through eval
• kernel-side integration:
  • model conversion language
  • unification
  • actually add in kernel
• _ at (n)
• indices:
  • get index from nth match of pattern
  • get position in AST from index
  • kernel side: apply red at index
• locus based reduction
• better error messages
  • wrong reduction type
  • wrong subargument (atomic abc currently says the reference atomic was not found in the current environment, which is misleading)
• tests
• documentation