From c5fe6cc2cada878ea3e70262e0c9b9f607db7974 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Tue, 7 Feb 2023 15:00:06 -0800
Subject: More comments

---
 tests/lean/hashmap_on_disk/Base/Primitives.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tests/lean')

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: "
-- 
cgit v1.2.3