search

Drup / dowsing

᚛ A type of divination employed in attempts to locate identifiers matching a given type expression
ISC License
35 stars 4 forks source link

Refine unifiers #4

Open Drup opened 3 years ago

Drup commented 3 years ago

Currently, the handling of unifiers is a bit rough:

  1. Unifier simplification simply "inlines" all the unnamed variables. It could do a bit more, like simplify alpha-conversions.
  2. Unnamed variables should be given fresh names before printing.
  3. The size function only counts the number of variables to be substituted, not the real size of the substitution.