search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

refactor: subst notation try to run isDefEq only once #4070

Closed nomeata closed 1 week ago

nomeata commented 1 week ago

there is already a isDefEq in ensureHasType and previously was another one after rewriting in hType. If we just always rewrite in hType, then we may get away with just one isDefEq.

nomeata commented 1 week ago

Not really a good idea, it can to rewriting twice where only once is desired.