diff options
Diffstat (limited to 'tests/lean/hashmap_on_disk/Base/Primitives.lean')
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 1f58851f..b201d81a 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -77,6 +77,10 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r +-- TODO: ideally, `let <--` would automatically pick the name for the fresh +-- hypothesis, of the form `h_x` where `x` is the name of the variable, with +-- collision-avoidance. That way, code generation would be simpler. + ---------------------- -- MACHINE INTEGERS -- ---------------------- @@ -362,6 +366,10 @@ open Lean Elab Command Term Meta syntax (name := assert) "#assert" term: command +-- TODO: figure out how to make #assert behave as #eval followed by a compiler +-- error if the term doesn't reduce to True. Once we have that, add some inline +-- tests for the arithmetic operations, notably `rem` + @[command_elab assert] def assertImpl : CommandElab := fun (_stx: Syntax) => do logInfo "Reducing and asserting: " |