We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 5cc4910 commit 1f8a3b2Copy full SHA for 1f8a3b2
Auto/Translation/Reduction.lean
@@ -9,6 +9,7 @@ private instance : ToString TransparencyMode where
9
| .default => "default"
10
| .reducible => "reducible"
11
| .instances => "instances"
12
+ | .none => "none"
13
14
private instance : Lean.KVMap.Value TransparencyMode where
15
toDataValue t := toString t
@@ -17,6 +18,7 @@ private instance : Lean.KVMap.Value TransparencyMode where
17
18
| "default" => some .default
19
| "reducible" => some .reducible
20
| "instances" => some .instances
21
+ | "none" => some .none
22
| _ => none
23
24
register_option auto.redMode : TransparencyMode := {
lean-toolchain
@@ -1 +1 @@
1
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0
0 commit comments