max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: typo

Browse source
This commit is contained in:
Leonardo de Moura 2024-01-02 05:17:20 -08:00 • committed by Sebastian Ullrich
parent e83e467667
commit b7efd200f0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
View file

@ -20,7 +20,7 @@ def fromExpr? (e : Expr) : SimpM (Option Value) := do
unless type.isAppOfArity ``Fin 1 do return none
let some size ← evalNat type.appArg! |>.run | return none
unless size > 0 do return none
let some value ← evalNat e.appFn!.appArg! |>.run | return none
let some value ← Nat.fromExpr? e.appFn!.appArg! | return none
let value := value % size
return some { size, value, ofNatFn := e.appFn!.appFn! }