| 6 | |
| 7 | |
| 8 | def main() -> None: |
| 9 | lake_dir = Path(__file__).resolve().parent.parent / "lean" |
| 10 | lib = LeanLibrary.from_lake(lake_dir, "Basic", build=True) |
| 11 | |
| 12 | print("py_increment(7) =", lib.increment(7)) |
| 13 | print('py_greet("world") =', lib.greet("world")) |
| 14 | print("py_sum_array([1..10]) =", lib.sumArray(list(range(1, 11)))) |
| 15 | print("py_origin(()) =", lib.origin(None)) |
| 16 | print("py_norm_sq((3, 4)) =", lib.normSq(lib.Point(3, 4))) |
| 17 | print("py_perimeter(circle 5) =", lib.perimeter(lib.Shape.circle(5))) |
| 18 | print("py_perimeter(square 4) =", lib.perimeter(lib.Shape.square(4))) |
| 19 | print("py_perimeter(rect 2 3) =", lib.perimeter(lib.Shape.rect(2, 3))) |
| 20 | |
| 21 | |
| 22 | if __name__ == "__main__": |