summaryrefslogtreecommitdiff
path: root/tests/coq/traits
diff options
context:
space:
mode:
authorRyan Lahfa2024-04-30 14:36:40 +0200
committerRyan Lahfa2024-04-30 14:36:40 +0200
commitb6a820cc3ed1d5d4d875cddf7982aaa84ff01d44 (patch)
tree9abbd4494d5d3da04b68c033568cd8bd80dc6cf4 /tests/coq/traits
parentfead40d1fb6e9f7bed705e8d3048133cf59c3bb8 (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 'tests/coq/traits')
0 files changed, 0 insertions, 0 deletions