aboutsummaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorKazuhiko Sakaguchi2019-08-30 11:30:21 +0200
committerKazuhiko Sakaguchi2019-10-30 23:19:33 +0100
commitd60c67b8f33f55e11ca159246d2a447102f10f20 (patch)
tree74fecfdcc5b2429e5cf199f9daa48a56540e2359 /.github
parentc5bd1d4d29021688db59495a8b60c84f5dea6b77 (diff)
Change the order of arguments in `ltngtP`
from `ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` to `ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions