search

aya-prover / aya-prover-proto

┗:smiley:┛ ┏:smiley:┓ ┗:smiley:┛
GNU General Public License v3.0
11 stars 0 forks source link

Refactor UntypedDefEq.java and TypedDefEq.java #734

Closed ericwang385 closed 3 years ago

ericwang385 commented 3 years ago

Merge java/org/aya/tyck/unify/UntypedDefEq.java and java/org/aya/tyck/unify/TypedDefEq.java into java/org/aya/tyck/unify/DefEq.java Try to delete Visitor in java/org/aya/core/term/Term.java but seems it was deeply bonded with the current term def so I give up for now.

ice1000 commented 3 years ago

Tests passed locally.

ice1000 commented 3 years ago

@ericwang385 what do you plan to do afterwards?

ericwang385 commented 3 years ago

@ericwang385 what do you plan to do afterwards?

Maybe first finish #658

After that, I wanna have a look at #722

If possible I wanna try the termination checking after all these low-hanging fruits.