Commit graph

3 commits

Author SHA1 Message Date
Leonardo de Moura
10c32fcf94 chore: HasToString => ToString 2020-10-27 16:11:48 -07:00
Leonardo de Moura
f176a7963c feat(library/init/lean/compiler/ir/emitcpp): register arity 0 declarations 2019-06-07 17:15:16 -07:00
Leonardo de Moura
3651dc7618 feat(library/init/lean): add evalConst
The implementation is good enough for implementing extensible parsers,
elaborators and tactics, but there are a few TODOs

1- We should have a better story for standalone applications.
   Most of them don't need `evalConst`, and the global table is
   just initialization overhead.

2- The global table introduces a dependency on the `Lean.Name`
   implementation. So, all standalone applications will depend on it.

3- We are not storing arity 0 constants in the table.
   This one should be easy to fix in the future.
2019-06-07 16:31:28 -07:00