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

chore: broken test after update stage0 (#8110)

Browse source 
This is a temporary fix for `master` after update stage0 breakage.

cc @Kha @nomeata
This commit is contained in:
Leonardo de Moura 2025-04-25 17:02:23 -07:00 • committed by GitHub
parent 882d1ab812
commit 60ee8c2f76
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/issue7408.lean
View file

@ -1,7 +1,8 @@
def computeFuel (mass : Nat) : Nat :=
let rec go acc cur :=
let n := cur / 3 - 2
if n = 0 then acc + cur else go (acc + cur) n
-- TODO: investigate why we need `_ :`
if _ : n = 0 then acc + cur else go (acc + cur) n
termination_by cur
go 0 mass - mass