1. 08 May, 2021 1 commit
  2. 05 May, 2021 1 commit
  3. 02 May, 2021 8 commits
  4. 01 May, 2021 1 commit
    • Kim Nguyễn's avatar
      Better fix for variable ordering: · e925dc34
      Kim Nguyễn authored
      When computing the result type of a function application ((t→s) • u)  with tallying,
      one first introduces a fresh variable 𝛾 and computes the tallying of
       (t → s) < (u → 𝛾)
      When solving the tallying constraints generated (if that step succeeds),
      variables are taken in some implementation defined order (variables created before
      have a smaller internal id). It is important then that the variables in u
      and 𝛾 are are all before the variables in t and s or all after.
      
      Otherwise, when computing the substitution, variables in u will depend on variables
      in t and s that will in turn depend on gamma (which gives unreadable types).
      e925dc34
  5. 30 Apr, 2021 4 commits
  6. 29 Apr, 2021 1 commit
  7. 28 Apr, 2021 3 commits
  8. 27 Apr, 2021 10 commits
  9. 26 Apr, 2021 10 commits
  10. 25 Apr, 2021 1 commit