Why not use unification

Open ice1000 opened this issue 3 years ago • 1 comments

https://github.com/aya-prover/aya-dev/blob/25089b867fc15648d82259e39a7b143f739bff2c/base/src/main/java/org/aya/generic/Shaped.java#L33-L56

@imkiva

Sep 21 '22 19:09 ice1000

I was stupid 🥺

Sep 21 '22 23:09 imkiva

I tried to rewrite this, but there is not enough stuff to construct a Unifier:

a Reporter (IgnoringReporter is usable though)
a SourcePos (Maybe SourcePos.NONE is usable if we use IgnoringReporter)
a TyckState (sameValue() is also used in PatMatcher which is unable to obtain a TyckState) (Note that the TyckState in this method is Nullable)

Oct 14 '22 18:10 HoshinoTented

Maybe a unifier does not need a reporter..

Oct 14 '22 23:10 ice1000

Oops

Oct 15 '22 00:10 ice1000

Ok I reimplemented this feature

Oct 15 '22 00:10 ice1000