We can use this primitive to process command line arguments of the form
`-D <key> = <value>`
TODO: allow users to attach `[init]` to definitions of the form
```
@[init] def foo : IO Unit := ...
```
and avoid the awkward auxiliary constant.
@kha I am finding the UTF8 API super useful. So, I am giving nice names
to it. The API is safe for users and the runtime implementation should
match the reference one.
The array read and write operations are now called:
- "Comfortable" version (with runtime bound checks):
`Array.get` and `Array.set` like OCaml.
It is also consistent with `Ref.get` and `Ref.put`,
and `get` and `set` for `MonadState`.
- `Fin` version (without runtime bound checks):
`Array.index` and `Array.update` like in F*.
- `USize` version (without runtime bound checks and unboxing):
`Array.idx` and `Array.updt`.
cc @kha
@kha I have added support for opaque constants to the old C++ frontend,
and made sure the new frontend can still parse `library/init/core.lean`.
The kernel should enforce that opaque constants are really opaque, and
the following example should fail
```
constant x : nat := 0
theorem foo : x = 0 := rfl
```
If it doesn't, it is a bug.
Here are some remaining issues:
1- `environment.mk_empty` is currently an axiom because we cannot create
an inhabitant of an opaque type. A possible solution is to use
`option environment` instead of `environment`.
2- There is no support for opaque constants in the new
frontend. However, I modified it to handle axioms, and fixed the literal
values with decl_cmd_kind. I tried to mark some of my changes with
comments, but it is probably much easier for you to just check the
commit change list.
3- I did not add any support for automatically constructing `e`
at `constant x : t := e`. I think we can do this later
after we replace the old frontend with the new one. BTW, it took only a
few minutes to provide the inhabitants manually.
The idea is to reuse the cell. The trick is like the one we used for
improving state_t. It seems to work pretty well. Now, the Lean
version is 29% slower than the C++ one.
cc @kha
