1 parent 9506def commit cef5eacCopy full SHA for cef5eac
2 files changed
Binary/Deriving.lean
@@ -1,9 +1,9 @@
1
module
2
3
-public meta import Lean
4
-import Binary.Basic
+public import Lean
+public import Binary.Basic
5
6
-public meta section
+public section
7
8
namespace Binary.Deriving
9
@@ -12,7 +12,7 @@ open Elab
12
open Deriving
13
open Meta hiding Context
14
open Term hiding Context
15
-open Command hiding Context
+open Elab.Command hiding Context
16
17
18
/--
@@ -236,7 +236,7 @@ where
236
let repr := assignment[ctorIdx]!
237
let stx ←
238
`(do
239
- if (← $(beInfo.decoder)) != $(quote repr) then
+ if (← $(beInfo.decoder):term) != $(quote repr) then
240
throw (DecodeError.userError "")
241
else
242
$[let $identNames:ident ← $decodes:doExpr]*
lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.32.0
0 commit comments