Ejecutar las pruebas
Para ejecutar las pruebas, asegúrate de tener instalado Lean 4.
Desde el directorio del ejercicio, ejecuta:
lake test
Resolver el ejercicio
La solución de un ejercicio es un módulo de Lean.
El nombre del módulo se define en una instrucción 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.
Este ExerciseName delante de someFun es un espacio de nombres, definido en el módulo con el mismo nombre, es decir, ExerciseName.
Esto significa que tienes que crear un archivo llamado ExerciseName.lean con este aspecto:
namespace ExerciseName
def someFun (someArg1 : Type1) (someArg2 : Type2) : ReturnType :=
...
end ExerciseName
Ten en cuenta que las pruebas suelen llamar a una o varias funciones con varios 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 devuelto de cada función tienen un tipo.
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 sitio en la misma carpeta que el módulo de pruebas.
Este archivo debería incluir un stub con la mayor parte de la información inicial, para que puedas usarlo como punto de partida para tu solución.
Ten en cuenta que este stub solo está ahí para que puedas empezar.
No dudes en 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, E/S y API del sistema, y otras utilidades básicas.
Esta importación debe estar 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 esta cualificación del espacio de nombres:
import Std
open Std
def someSet : TreeSet String := ...
Los paquetes externos no están disponibles directamente y deben añadirse como dependencia en lakefile.toml.
Cuando trabajas en local, puedes usar el paquete que quieras.
Sin embargo, el ejecutor de pruebas en línea solo tiene acceso a la biblioteca estándar Std.
