JovanGerb
JovanGerb
To be honest, I'm not yet convinced that the new location syntax is needed, because if you want to do something at specific locations in multiple different hypotheses, then you...
I have code that allows these patterns to also include bound variables. Would it be better to add it to this PR or to put it in a later PR?...
I cleaned up this PR a while ago, but I didn't put it on awaiting-review, because I wasn't sure whether this should really be included into batteries. It seems to...
I think so. The main observation making this PR redundant is that if you want to do a rewrite which holds definitionally, then you can do this via `rw [show...
I tried an implementation with MLList, where I manually made a new version of withLocalDeclD that works with MLList, but building the DiscrTree then takes 4x longer, so that doesn't...
awaiting-review
In terms of which one is preferred, I think there is no real reason to prefer the old implementation, other than that porting to a new version might take a...
I heard that the `exact?` tactic will soon be moving to Std, and it would be great to get that running with the new `DiscrTree`. Our next goal is to...
I just ran a test comparing building the old and new version of `DiscrTree`, using heartbeats. The new version takes 1.27 times as many heartbeats compared to the old version....
I added an argument `(unify : Bool)` to the unification/lookup function. By setting this to false, you can instruct the lookup algorithm to treat metavariables as free variables. The old...