Skip to content

feat: use cbv in several examples #304

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
TwoFX merged 1 commit into from
Mar 26, 2026
Merged

feat: use cbv in several examples #304

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions HumanEvalLean/HumanEval0.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,13 +33,13 @@ def hasCloseElements (xs : Array Rat) (threshold : Rat) : Bool := Id.run do
## Tests
-/

example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by native_decide
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by native_decide
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by native_decide
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by native_decide
example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by native_decide
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by native_decide
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by native_decide
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by cbv
example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by cbv
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by cbv
example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by cbv
example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by cbv
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by cbv
example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by cbv

/-!
## Verification
Expand Down
24 changes: 12 additions & 12 deletions HumanEvalLean/HumanEval106.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,10 +38,10 @@ def f (n : Nat) : List Nat := Id.run do
### Tests
-/

example : f 5 = [1, 2, 6, 24, 15] := by native_decide
example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by native_decide
example : f 1 = [1] := by native_decide
example : f 3 = [1, 2, 6] := by native_decide
example : f 5 = [1, 2, 6, 24, 15] := by cbv
example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by cbv
example : f 1 = [1] := by cbv
example : f 3 = [1, 2, 6] := by cbv

/-!
### Verification
Expand Down Expand Up @@ -134,10 +134,10 @@ def f' (n : Nat) : Array Nat := Id.run do
### Tests
-/

example : f' 5 = #[1, 2, 6, 24, 15] := by native_decide
example : f' 7 = #[1, 2, 6, 24, 15, 720, 28] := by native_decide
example : f' 1 = #[1] := by native_decide
example : f' 3 = #[1, 2, 6] := by native_decide
example : f' 5 = #[1, 2, 6, 24, 15] := by cbv
example : f' 7 = #[1, 2, 6, 24, 15, 720, 28] := by cbv
example : f' 1 = #[1] := by cbv
example : f' 3 = #[1, 2, 6] := by cbv

/-!
### Verification
Expand Down Expand Up @@ -204,10 +204,10 @@ def f'' (n : Nat) : Array Nat := Id.run do
### Tests
-/

example : f'' 5 = #[1, 2, 6, 24, 15] := by native_decide
example : f'' 7 = #[1, 2, 6, 24, 15, 720, 28] := by native_decide
example : f'' 1 = #[1] := by native_decide
example : f'' 3 = #[1, 2, 6] := by native_decide
example : f'' 5 = #[1, 2, 6, 24, 15] := by cbv
example : f'' 7 = #[1, 2, 6, 24, 15, 720, 28] := by cbv
example : f'' 1 = #[1] := by cbv
example : f'' 3 = #[1, 2, 6] := by cbv

/-!
### Verification
Expand Down
10 changes: 5 additions & 5 deletions HumanEvalLean/HumanEval115.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,11 @@ def maxFill (grid : Vector (Vector Nat n) m) (capacity : Nat) : Nat :=
# Tests
-/

example : maxFill #v[#v[0,0,1,0], #v[0,1,0,0], #v[1,1,1,1]] 1 = 6 := by native_decide
example : maxFill #v[#v[0,0,1,1], #v[0,0,0,0], #v[1,1,1,1], #v[0,1,1,1]] 2 = 5 := by native_decide
example : maxFill #v[#v[0,0,0], #v[0,0,0]] 5 = 0 := by native_decide
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 2 = 4 := by native_decide
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 9 = 2 := by native_decide
example : maxFill #v[#v[0,0,1,0], #v[0,1,0,0], #v[1,1,1,1]] 1 = 6 := by cbv
example : maxFill #v[#v[0,0,1,1], #v[0,0,0,0], #v[1,1,1,1], #v[0,1,1,1]] 2 = 5 := by cbv
example : maxFill #v[#v[0,0,0], #v[0,0,0]] 5 = 0 := by cbv
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 2 = 4 := by cbv
example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]] 9 = 2 := by cbv

/-!
## Verification
Expand Down
6 changes: 3 additions & 3 deletions HumanEvalLean/HumanEval12.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@ def longest? (xs : List String) : Option String :=
## Tests
-/

example : longest? [] = none := by native_decide
example : longest? ["x", "y", "z"] = some "x" := by native_decide
example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by native_decide
example : longest? [] = none := by cbv
example : longest? ["x", "y", "z"] = some "x" := by cbv
example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by cbv

/-!
## Verification
Expand Down
10 changes: 5 additions & 5 deletions HumanEvalLean/HumanEval122.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,11 @@ def addElements (xs : Array Int) (k : Nat) : Int :=
## Tests
-/

example : addElements #[1,-2,-3,41,57,76,87,88,99] 3 = -4 := by native_decide
example : addElements #[111,121,3,4000,5,6] 2 = 0 := by native_decide
example : addElements #[11,21,3,90,5,6,7,8,9] 4 = 125 := by native_decide
example : addElements #[111,21,3,4000,5,6,7,8,9] 4 = 24 := by native_decide
example : addElements #[1] 1 = 1 := by native_decide
example : addElements #[1,-2,-3,41,57,76,87,88,99] 3 = -4 := by cbv
example : addElements #[111,121,3,4000,5,6] 2 = 0 := by cbv
example : addElements #[11,21,3,90,5,6,7,8,9] 4 = 125 := by cbv
example : addElements #[111,21,3,4000,5,6,7,8,9] 4 = 24 := by cbv
example : addElements #[1] 1 = 1 := by cbv

/-!
## Verification
Expand Down
16 changes: 8 additions & 8 deletions HumanEvalLean/HumanEval128.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,14 +68,14 @@ def prodSigns (arr : List Int) : Option Int := do
## Tests
-/

example : prodSigns [1, 2, 2, -4] = some (-9) := by native_decide
example : prodSigns [0, 1] = some 0 := by native_decide
example : prodSigns [] = none := by native_decide
example : prodSigns [1, 1, 1, 2, 3, -1, 1] = some (-10) := by native_decide
example : prodSigns [2, 4, 1, 2, -1, -1, 9] = some 20 := by native_decide
example : prodSigns [-1, 1, -1, 1] = some 4 := by native_decide
example : prodSigns [-1, 1, 1, 1] = some (-4) := by native_decide
example : prodSigns [-1, 1, 1, 0] = some 0 := by native_decide
example : prodSigns [1, 2, 2, -4] = some (-9) := by cbv
example : prodSigns [0, 1] = some 0 := by cbv
example : prodSigns [] = none := by cbv
example : prodSigns [1, 1, 1, 2, 3, -1, 1] = some (-10) := by cbv
example : prodSigns [2, 4, 1, 2, -1, -1, 9] = some 20 := by cbv
example : prodSigns [-1, 1, -1, 1] = some 4 := by cbv
example : prodSigns [-1, 1, 1, 1] = some (-4) := by cbv
example : prodSigns [-1, 1, 1, 0] = some 0 := by cbv

/-!
## Verification
Expand Down
8 changes: 4 additions & 4 deletions HumanEvalLean/HumanEval13.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@ There is nothing to implement: The standard library provides `Int.gcd` out of th
## Tests
-/

example : Int.gcd 3 7 = 1 := by native_decide
example : Int.gcd 10 15 = 5 := by native_decide
example : Int.gcd 49 14 = 7 := by native_decide
example : Int.gcd 144 60 = 12 := by native_decide
example : Int.gcd 3 7 = 1 := by cbv
example : Int.gcd 10 15 = 5 := by cbv
example : Int.gcd 49 14 = 7 := by cbv
example : Int.gcd 144 60 = 12 := by cbv

/-!
## Verification
Expand Down
24 changes: 12 additions & 12 deletions HumanEvalLean/HumanEval133.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 +5,18 @@ def sumSquares (xs : List Rat) : Int :=

/-! ## Tests -/

example : sumSquares [1, 2, 3] = 14 := by native_decide
example : sumSquares [1.0, 2, 3] = 14 := by native_decide
example : sumSquares [1, 3, 5, 7] = 84 := by native_decide
example : sumSquares [1.4, 4.2, 0] = 29 := by native_decide
example : sumSquares [-2.4, 1, 1] = 6 := by native_decide
example : sumSquares [100, 1, 15, 2] = 10230 := by native_decide
example : sumSquares [10000, 10000] = 200000000 := by native_decide
example : sumSquares [-1.4, 4.6, 6.3] = 75 := by native_decide
example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by native_decide
example : sumSquares [0] = 0 := by native_decide
example : sumSquares [-1] = 1 := by native_decide
example : sumSquares [-1, 1, 0] = 2 := by native_decide
example : sumSquares [1, 2, 3] = 14 := by cbv
example : sumSquares [1.0, 2, 3] = 14 := by cbv
example : sumSquares [1, 3, 5, 7] = 84 := by cbv
example : sumSquares [1.4, 4.2, 0] = 29 := by cbv
example : sumSquares [-2.4, 1, 1] = 6 := by cbv
example : sumSquares [100, 1, 15, 2] = 10230 := by cbv
example : sumSquares [10000, 10000] = 200000000 := by cbv
example : sumSquares [-1.4, 4.6, 6.3] = 75 := by cbv
example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by cbv
example : sumSquares [0] = 0 := by cbv
example : sumSquares [-1] = 1 := by cbv
example : sumSquares [-1, 1, 0] = 2 := by cbv

/-!
## Verification
Expand Down
8 changes: 4 additions & 4 deletions HumanEvalLean/HumanEval139.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,10 +45,10 @@ theorem special_factorial_func_correct {n : Nat} :
apply this <;> simp [Nat.factorial, Nat.brazilianFactorial]
intros; fun_induction special_factorial.go <;> grind [Nat.factorial, Nat.brazilianFactorial]

theorem test1 : special_factorial 4 = 288 := by native_decide
theorem test2 : special_factorial 5 = 34560 := by native_decide
theorem test3 : special_factorial 7 = 125411328000 := by native_decide
theorem test4 : special_factorial 1 = 1 := by native_decide
theorem test1 : special_factorial 4 = 288 := by cbv
theorem test2 : special_factorial 5 = 34560 := by cbv
theorem test3 : special_factorial 7 = 125411328000 := by cbv
theorem test4 : special_factorial 1 = 1 := by cbv

/-!
## Prompt
Expand Down
6 changes: 3 additions & 3 deletions HumanEvalLean/HumanEval2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ def truncateNumber (x : Rat) : Rat :=
## Tests
-/

example : truncateNumber (7/2) = 1/2 := by native_decide
example : truncateNumber (133/100) = 33/100 := by native_decide
example : truncateNumber (123456/1000) = 456/1000 := by native_decide
example : truncateNumber (7/2) = 1/2 := by cbv
example : truncateNumber (133/100) = 33/100 := by cbv
example : truncateNumber (123456/1000) = 456/1000 := by cbv

/-!
## Verification
Expand Down
6 changes: 3 additions & 3 deletions HumanEvalLean/HumanEval22.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,9 @@ def filterIntegers (xs : Array Any): Array Int :=

/-! ## Tests -/

example : filterIntegers #[] = #[] := by native_decide
example : filterIntegers #[.int 4, .float 23.2, .int 9, .string "adasd"] = #[4, 9] := by native_decide
example : filterIntegers #[.int 3, .string "c", .int 3, .int 3, .string "a", .string "b"] = #[3, 3, 3] := by native_decide
example : filterIntegers #[] = #[] := by cbv
example : filterIntegers #[.int 4, .float 23.2, .int 9, .string "adasd"] = #[4, 9] := by cbv
example : filterIntegers #[.int 3, .string "c", .int 3, .int 3, .string "a", .string "b"] = #[3, 3, 3] := by cbv

/-! ## Verification -/

Expand Down
10 changes: 5 additions & 5 deletions HumanEvalLean/HumanEval24.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,11 @@ where
| i + 2 => exact Nat.lt_of_lt_of_le (Nat.lt_mul_self_iff.2 (by omega)) (Nat.not_lt.1 h)
omega

example : largestDivisor 3 = 1 := by native_decide
example : largestDivisor 7 = 1 := by native_decide
example : largestDivisor 10 = 5 := by native_decide
example : largestDivisor 100 = 50 := by native_decide
example : largestDivisor 49 = 7 := by native_decide
example : largestDivisor 3 = 1 := by cbv
example : largestDivisor 7 = 1 := by cbv
example : largestDivisor 10 = 5 := by cbv
example : largestDivisor 100 = 50 := by cbv
example : largestDivisor 49 = 7 := by cbv

inductive LargestDivisorSpec (n : Nat) : Nat → Prop
| one : (∀ j, 2 ≤ j → j * j ≤ n → n % j ≠ 0) → LargestDivisorSpec n 1
Expand Down
20 changes: 10 additions & 10 deletions HumanEvalLean/HumanEval25.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,16 @@ def factorize (x : Nat) : Array Nat :=

/-! ## Tests -/

example : factorize 2 = #[2] := by native_decide
example : factorize 4 = #[2, 2] := by native_decide
example : factorize 8 = #[2, 2, 2] := by native_decide
example : factorize 25 = #[5, 5] := by native_decide
example : factorize 70 = #[2, 5, 7] := by native_decide
example : factorize 57 = #[3, 19] := by native_decide
example : factorize 3249 = #[3, 3, 19, 19] := by native_decide
example : factorize 185193 = #[3, 3, 3, 19, 19, 19] := by native_decide
example : factorize 20577 = #[3, 19, 19, 19] := by native_decide
example : factorize 18 = #[2, 3, 3] := by native_decide
example : factorize 2 = #[2] := by cbv
example : factorize 4 = #[2, 2] := by cbv
example : factorize 8 = #[2, 2, 2] := by cbv
example : factorize 25 = #[5, 5] := by cbv
example : factorize 70 = #[2, 5, 7] := by cbv
example : factorize 57 = #[3, 19] := by cbv
example : factorize 3249 = #[3, 3, 19, 19] := by cbv
example : factorize 185193 = #[3, 3, 3, 19, 19, 19] := by cbv
example : factorize 20577 = #[3, 19, 19, 19] := by cbv
example : factorize 18 = #[2, 3, 3] := by cbv

/-! ## Verification -/

Expand Down
6 changes: 3 additions & 3 deletions HumanEvalLean/HumanEval26.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,9 @@ def removeDuplicates (xs : Array Int) : Array Int :=

/-! ## Tests -/

example : removeDuplicates #[] = #[] := by native_decide
example : removeDuplicates #[1, 2, 3, 4] = #[1, 2, 3, 4] := by native_decide
example : removeDuplicates #[1, 2, 3, 2, 4, 3, 5] = #[1, 4, 5] := by native_decide
example : removeDuplicates #[] = #[] := by cbv
example : removeDuplicates #[1, 2, 3, 4] = #[1, 2, 3, 4] := by cbv
example : removeDuplicates #[1, 2, 3, 2, 4, 3, 5] = #[1, 4, 5] := by cbv

/-! ## Missing API -/

Expand Down
8 changes: 4 additions & 4 deletions HumanEvalLean/HumanEval30.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,10 @@ def getPositive (xs : Array Int): Array Int :=

/-! ## Tests -/

example : getPositive #[-1, -2, 4, 5, 6] = #[4, 5, 6] := by native_decide
example : getPositive #[5, 3, -5, 2, 3, 3, 9, 0, 123, 1, -10] = #[5, 3, 2, 3, 3, 9, 123, 1] := by native_decide
example : getPositive #[-1, -2] = #[] := by native_decide
example : getPositive #[] = #[] := by native_decide
example : getPositive #[-1, -2, 4, 5, 6] = #[4, 5, 6] := by cbv
example : getPositive #[5, 3, -5, 2, 3, 3, 9, 0, 123, 1, -10] = #[5, 3, 2, 3, 3, 9, 123, 1] := by cbv
example : getPositive #[-1, -2] = #[] := by cbv
example : getPositive #[] = #[] := by cbv

/-! ## Verification -/

Expand Down
6 changes: 3 additions & 3 deletions HumanEvalLean/HumanEval4.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,9 @@ def meanAbsoluteDeviation (xs : Array Rat) : Rat :=

/-! ## Tests -/

example : meanAbsoluteDeviation #[(1 : Rat), 2, 3] = (2 : Rat) / 3 := by native_decide
example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4] = 1 := by native_decide
example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4, 5] = (6 : Rat) / 5 := by native_decide
example : meanAbsoluteDeviation #[(1 : Rat), 2, 3] = (2 : Rat) / 3 := by cbv
example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4] = 1 := by cbv
example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4, 5] = (6 : Rat) / 5 := by cbv

/-!
## Verification
Expand Down
36 changes: 18 additions & 18 deletions HumanEvalLean/HumanEval40.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,15 +28,15 @@ public def triplesSumToZero (xs : Array Int) : Bool := Id.run do

/-! ## Tests 1 -/

example : triplesSumToZero #[1, 3, 5, 0] = false := by native_decide
example : triplesSumToZero #[1, 3, 5, -1] = false := by native_decide
example : triplesSumToZero #[1, 3, -2, 1] = true := by native_decide
example : triplesSumToZero #[1, 2, 3, 7] = false := by native_decide
example : triplesSumToZero #[1, 2, 5, 7] = false := by native_decide
example : triplesSumToZero #[2, 4, -5, 3, 9, 7] = true := by native_decide
example : triplesSumToZero #[1] = false := by native_decide
example : triplesSumToZero #[1, 3, 5, -100] = false := by native_decide
example : triplesSumToZero #[100, 3, 5, -100] = false := by native_decide
example : triplesSumToZero #[1, 3, 5, 0] = false := by cbv
example : triplesSumToZero #[1, 3, 5, -1] = false := by cbv
example : triplesSumToZero #[1, 3, -2, 1] = true := by cbv
example : triplesSumToZero #[1, 2, 3, 7] = false := by cbv
example : triplesSumToZero #[1, 2, 5, 7] = false := by cbv
example : triplesSumToZero #[2, 4, -5, 3, 9, 7] = true := by cbv
example : triplesSumToZero #[1] = false := by cbv
example : triplesSumToZero #[1, 3, 5, -100] = false := by cbv
example : triplesSumToZero #[100, 3, 5, -100] = false := by cbv

/-! ## Missing API -/

Expand Down Expand Up @@ -134,15 +134,15 @@ where

/-! ## Tests 2 -/

example : triplesSumToZero' #[1, 3, 5, 0] = false := by native_decide
example : triplesSumToZero' #[1, 3, 5, -1] = false := by native_decide
example : triplesSumToZero' #[1, 3, -2, 1] = true := by native_decide
example : triplesSumToZero' #[1, 2, 3, 7] = false := by native_decide
example : triplesSumToZero' #[1, 2, 5, 7] = false := by native_decide
example : triplesSumToZero' #[2, 4, -5, 3, 9, 7] = true := by native_decide
example : triplesSumToZero' #[1] = false := by native_decide
example : triplesSumToZero' #[1, 3, 5, -100] = false := by native_decide
example : triplesSumToZero' #[100, 3, 5, -100] = false := by native_decide
example : triplesSumToZero' #[1, 3, 5, 0] = false := by cbv
example : triplesSumToZero' #[1, 3, 5, -1] = false := by cbv
example : triplesSumToZero' #[1, 3, -2, 1] = true := by cbv
example : triplesSumToZero' #[1, 2, 3, 7] = false := by cbv
example : triplesSumToZero' #[1, 2, 5, 7] = false := by cbv
example : triplesSumToZero' #[2, 4, -5, 3, 9, 7] = true := by cbv
example : triplesSumToZero' #[1] = false := by cbv
example : triplesSumToZero' #[1, 3, 5, -100] = false := by cbv
example : triplesSumToZero' #[100, 3, 5, -100] = false := by cbv

/-! ## Verification 2 -/

Expand Down
6 changes: 3 additions & 3 deletions HumanEvalLean/HumanEval45.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,9 @@ def triangleArea (a h : Rat) : Rat :=

/-! ## Tests -/

example : triangleArea 5 3 = 7.5 := by native_decide
example : triangleArea 2 2 = 2.0 := by native_decide
example : triangleArea 10 8 = 40.0 := by native_decide
example : triangleArea 5 3 = 7.5 := by cbv
example : triangleArea 2 2 = 2.0 := by cbv
example : triangleArea 10 8 = 40.0 := by cbv

/-!
## Verification
Expand Down
8 changes: 4 additions & 4 deletions HumanEvalLean/HumanEval46.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@ def fib4 (n : Nat) : Nat := Id.run do

/-! ## Tests -/

example : fib4 5 = 4 := by native_decide
example : fib4 8 = 28 := by native_decide
example : fib4 10 = 104 := by native_decide
example : fib4 12 = 386 := by native_decide
example : fib4 5 = 4 := by cbv
example : fib4 8 = 28 := by cbv
example : fib4 10 = 104 := by cbv
example : fib4 12 = 386 := by cbv

/-! ## Missing API -/

Expand Down
Loading
Loading
⚡