Probar en la ruta de Lean

Ejecutar las pruebas

Para ejecutar las pruebas, asegúrate de que tengas instalado Lean 4.

Desde el directorio del ejercicio, ejecuta:

lake test

Resolver el ejercicio

Una solución a un ejercicio es un módulo de Lean. El nombre del módulo se define en una sentencia de importación al principio del conjunto de pruebas:

import LeanTest
import ExerciseName

open LeanTest

def exerciseNameTests : TestSuite :=
  (TestSuite.empty "ExerciseName")
  |>.addTest "first test" (do
        return assertEqual someVal (ExerciseName.someFun someArg1 someArg2))
    ...

def main : IO UInt32 := do
  runTestSuitesWithExitCode [exerciseNameTests]

En este ejemplo, el archivo de pruebas importa, en la línea 2, un módulo llamado ExerciseName. La prueba first test llama a una función ExerciseName.someFun con los argumentos someArg1 y someArg2. Ese ExerciseName antes de someFun es un espacio de nombres, definido en el módulo con el mismo nombre, es decir, ExerciseName. Esto significa que debes crear un archivo llamado ExerciseName.lean que se vea así:

namespace ExerciseName

def someFun (someArg1 : Type1) (someArg2 : Type2) : ReturnType :=
    ...

end ExerciseName

Fíjate que las pruebas normalmente llaman a una o más funciones con cierto número de argumentos. Se espera que todas ellas estén definidas en el módulo de la solución, dentro de un espacio de nombres con el mismo nombre que el módulo.

Cada argumento y el valor de retorno de cada función tiene algún tipo. Este puede ser uno de los tipos básicos de Lean (por ejemplo, Nat, List Int u Option String), o un tipo definido por el usuario.

Encontrarás un archivo con el nombre correcto ya en su lugar, en la misma carpeta que el módulo de pruebas. Este archivo debería tener un stub con la mayor parte de la información inicial, para que puedas usarlo como punto de partida para tu solución.

Solo ten en cuenta que este stub está ahí solo para que empieces. Siéntete libre de cambiarlo por completo si crees que es lo correcto.

Usar paquetes

Los proyectos de Lean que usan Lake siempre pueden importar la biblioteca estándar Std, que contiene estructuras de datos adicionales, API de E/S y del sistema, y otras utilidades básicas. Esta importación debe ir al principio del archivo:

import Std

def someMap : Std.HashMap Int Nat := ...

En este ejemplo, el tipo HashMap está cualificado con Std, el espacio de nombres donde se define. Todos los recursos de la biblioteca estándar están en el mismo espacio de nombres, Std.

También es posible abrir un módulo para que todas sus estructuras de datos y funciones estén disponibles sin esa cualificación del espacio de nombres:

import Std

open Std

def someSet : TreeSet String := ...

Los paquetes externos no están disponibles directamente y deben agregarse como dependencia en lakefile.toml.

Mientras trabajas de forma local, puedes usar cualquier paquete que quieras. Sin embargo, el ejecutor de pruebas en línea solo tiene acceso a la biblioteca estándar Std.