search

aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
278 stars 16 forks source link

Callable.Tele with empty args could have a shared instance #1099

Closed ice1000 closed 3 months ago

ice1000 commented 3 months ago

Should be stored in the JitDef, and we always use it rather than new a call with empty seq

ice1000 commented 3 months ago

Maybe what we want to do is hashconsing

ice1000 commented 3 months ago

IDK 💀