File tree Expand file tree Collapse file tree 1 file changed +3
-3
lines changed
src/Lean/Compiler/LCNF/Simp Expand file tree Collapse file tree 1 file changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -311,7 +311,7 @@ def Folder.mulShift [Literal α] [BEq α] (shiftLeft : Name) (pow2 : α → α)
311311-- TODO: add option for controlling the limit
312312def natPowThreshold := 256
313313
314- def foldNatPow (args : Array Arg): FolderM (Option LetValue) := do
314+ def foldNatPow (args : Array Arg) : FolderM (Option LetValue) := do
315315 let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
316316 let some value₁ ← getNatLit fvarId₁ | return none
317317 let some value₂ ← getNatLit fvarId₂ | return none
@@ -323,12 +323,12 @@ def foldNatPow (args : Array Arg): FolderM (Option LetValue) := do
323323/--
324324Folder for ofNat operations on fixed-sized integer types.
325325-/
326- def Folder.ofNat (f : Nat → LitValue) (args : Array Arg): FolderM (Option LetValue) := do
326+ def Folder.ofNat (f : Nat → LitValue) (args : Array Arg) : FolderM (Option LetValue) := do
327327 let #[.fvar fvarId] := args | return none
328328 let some value ← getNatLit fvarId | return none
329329 return some (.lit (f value))
330330
331- def Folder.toNat (args : Array Arg): FolderM (Option LetValue) := do
331+ def Folder.toNat (args : Array Arg) : FolderM (Option LetValue) := do
332332 let #[.fvar fvarId] := args | return none
333333 let some (.lit lit) ← findLetValue? fvarId | return none
334334 match lit with
You can’t perform that action at this time.
0 commit comments