summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-03-07 08:41:57 +0100
committerSon HO2023-06-04 21:44:33 +0200
commitfeb60683216a6d9193d6353605560c6c80a1ab41 (patch)
tree222f61e4c5cbcd166e81d82350afc54b002774df /backends
parentb4bad8df4eabb17c71dfa7b24d79d62fc06d0a70 (diff)
Make minor modifications and regenerate the Lean files
Diffstat (limited to 'backends')
-rw-r--r--backends/lean/Primitives.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Primitives.lean b/backends/lean/Primitives.lean
index e558e476..346e4b89 100644
--- a/backends/lean/Primitives.lean
+++ b/backends/lean/Primitives.lean
@@ -21,7 +21,7 @@ open Error
inductive Result (α : Type u) where
| ret (v: α): Result α
- | fail (e: Error): Result α
+ | fail (e: Error): Result α
deriving Repr, BEq
open Result