diff options
| author | Ryan Lahfa | 2024-04-30 14:36:40 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-04-30 14:36:40 +0200 |
| commit | b6a820cc3ed1d5d4d875cddf7982aaa84ff01d44 (patch) | |
| tree | 9abbd4494d5d3da04b68c033568cd8bd80dc6cf4 /tests/coq/arrays/Arrays.v | |
| parent | fead40d1fb6e9f7bed705e8d3048133cf59c3bb8 (diff) | |
feat(backend/lean): Raw Lean literals can be parsed into scalars automatically
We can use coercion to go to integers, build a scalar out of an int via
unification and let the user clear up bounds or let Lean decide them.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions