summaryrefslogtreecommitdiff
path: root/compiler/InterpreterPaths.ml
diff options
context:
space:
mode:
authorSon HO2024-06-22 13:22:32 +0200
committerGitHub2024-06-22 13:22:32 +0200
commit8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c (patch)
treeb3de971e89c369f30de349806c87913edeb17333 /compiler/InterpreterPaths.ml
parent4d30546c809cb2c512e0c3fd8ee540fff1330eab (diff)
Improve `scalar_tac` and `scalar_decr_tac` (#256)
* Fix an issue in a proof of the hashmap * Improve scalar_decr_tac * Improve the error message of scalar_tac and add the missing Termination.lean
Diffstat (limited to 'compiler/InterpreterPaths.ml')
0 files changed, 0 insertions, 0 deletions