diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index 1185a07d..117f76a2 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -60,12 +60,12 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) := /- HELPERS -/ -def ret? {α: Type} (r: Result α): Bool := +def ret? {α: Type u} (r: Result α): Bool := match r with | ret _ => true | fail _ | div => false -def div? {α: Type} (r: Result α): Bool := +def div? {α: Type u} (r: Result α): Bool := match r with | div => true | ret _ | fail _ => false @@ -73,14 +73,14 @@ def div? {α: Type} (r: Result α): Bool := def massert (b:Bool) : Result Unit := if b then ret () else fail assertionFailure -def eval_global {α: Type} (x: Result α) (_: ret? x): α := +def eval_global {α: Type u} (x: Result α) (_: ret? x): α := match x with | fail _ | div => by contradiction | ret x => x /- DO-DSL SUPPORT -/ -def bind (x: Result α) (f: α -> Result β) : Result β := +def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β := match x with | ret v => f v | fail v => fail v @@ -111,23 +111,6 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := | fail e => fail e | div => div -macro "let" e:term " ⟵ " f:term : doElem => - `(doElem| let ⟨$e, h⟩ ← Result.attach $f) - --- TODO: any way to factorize both definitions? -macro "let" e:term " <-- " f:term : doElem => - `(doElem| let ⟨$e, h⟩ ← Result.attach $f) - --- We call the hypothesis `h`, in effect making it unavailable to the user --- (because too much shadowing). But in practice, once can use the French single --- quote notation (input with f< and f>), where `‹ h ›` finds a suitable --- hypothesis in the context, this is equivalent to `have x: h := by assumption in x` -#eval do - let y <-- .ret (0: Nat) - let _: y = 0 := by cases ‹ ret 0 = ret y › ; decide - let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ - .ret r - @[simp] theorem bind_tc_ret (x : α) (f : α → Result β) : (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind] |