Lean → codice

lungo

Genera Rust, C, Go, Python, Swift e TypeScript da normali progetti Lake. Lean controlla e compila il programma; lungo lo esegue su un unico runtime dietro un’API idiomatica in ogni linguaggio.

Scarica lungo

Tutti i download Configurazione Errori Tutta la documentazione

Lean · lean/Shapes.lean

structure Rect where
  width : Nat
  height : Nat

def area (r : Rect) : Nat := r.width * r.height

theorem area_scale (k : Nat) (r : Rect) :
    area (scale k r) = k * k * area r := by
  simp only [area, scale]
  rw [Nat.mul_mul_mul_comm]

lungo lo compila nel crate

Rust · tests/rect.rs

let r = Rect { width: Nat::from(3u64), height: Nat::from(4u64) };
assert_eq!(area(r), Nat::from(12u64));

Una riga in build.rs

compile_lean("lean") compila i target predefiniti del progetto Lake e genera un modulo Rust che prende il nome dal pacchetto.

Controllato da Lean

Lean elabora il progetto e lo fa controllare dal kernel; una dimostrazione falsa o un Lean non valido fanno fallire la build.

Nessun runtime di Lean

Il codice compilato gira su un port in Rust del runtime di Lean, compilato dentro i crate Rust o precompilato per ogni altro linguaggio.

API idiomatiche

Le structure Lean diventano struct Rust, struct Go, dataclass Python, struct Swift, oggetti TypeScript; Nat un intero illimitato; IO un errore.

Ogni linguaggio, un runtime

lungo generate scrive pacchetti Go, Python, Swift, TypeScript e C che girano sul runtime precompilato, verificati tramite SHA-256.