PLDB
Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon

Lean

Lean

Lean is a pl created in 2015.

#186on PLDB 7Years Old 2.9kUsers
4Books 10Papers 2kRepos

Try now: TIO

Lean Theorem Prover


Example from hello-world:
#print "Hello World"
Example from Linguist:
/- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: algebra.binary Authors: Leonardo de Moura, Jeremy Avigad General properties of binary operations. -/ import logic.eq open eq.ops namespace binary section variable {A : Type} variables (op₁ : A → A → A) (inv : A → A) (one : A) local notation a * b := op₁ a b local notation a ⁻¹ := inv a local notation 1 := one definition commutative := ∀a b, a * b = b * a definition associative := ∀a b c, (a * b) * c = a * (b * c) definition left_identity := ∀a, 1 * a = a definition right_identity := ∀a, a * 1 = a definition left_inverse := ∀a, a⁻¹ * a = 1 definition right_inverse := ∀a, a * a⁻¹ = 1 definition left_cancelative := ∀a b c, a * b = a * c → b = c definition right_cancelative := ∀a b c, a * b = c * b → a = c definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b = a definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a variable (op₂ : A → A → A) local notation a + b := op₂ a b definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c end context variable {A : Type} variable {f : A → A → A} variable H_comm : commutative f variable H_assoc : associative f infixl `*` := f theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) := take a b c, calc a*(b*c) = (a*b)*c : H_assoc ... = (b*a)*c : H_comm ... = b*(a*c) : H_assoc theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b := take a b c, calc (a*b)*c = a*(b*c) : H_assoc ... = a*(c*b) : H_comm ... = (a*c)*b : H_assoc end context variable {A : Type} variable {f : A → A → A} variable H_assoc : associative f infixl `*` := f theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) := calc (a*b)*(c*d) = a*(b*(c*d)) : H_assoc ... = a*((b*c)*d) : H_assoc end end binary

Language features

Feature Supported Example Token
Comments
Line Comments
Integers
Strings
"Hello world"
"
Print() Debugging #print

Books about Lean from ISBNdb

title authors year publisher
Functional Programming Patterns in Scala and Clojure: Write Lean Programs for the JVM Bevilacqua-Linn, Michael 2013 Pragmatic Bookshelf
Measuring and Improving Performance: Information Technology Applications in Lean Systems Martin, James William 2009 CRC Press
Lean Python: Learn Just Enough Python to Build Useful Tools Gerrard, Paul 2016 Apress
Lean Software Systems Engineering for Developers: Managing Requirements, Complexity, Teams, and Change Like a Champ Durham, Doug and Michel, Chad 2021 Apress

Publications about Lean from Semantic Scholar

title authors year citations influentialCitations
Exploring the role of human factors in lean management P. Gaiardelli and Barbara Resta and Stefano Dotti 2019 32 2
Development of a Lean Computational Thinking Abilities Assessment for Middle Grades Students E. Wiebe and Jennifer E. London and Osman Aksit and Bradford W. Mott and K. Boyer and James C. Lester 2019 31 4
Lean management approach in hospitals: a systematic review Haleh Mousavi Isfahani and S. Tourani and H. Seyedin 2019 22 3
Memory-Efficient Performance Monitoring on Programmable Switches with Lean Algorithms Zaoxing Liu and Samson Zhou and Ori Rottenstreich and V. Braverman and J. Rexford 2019 20 0
The Lean 4 Theorem Prover and Programming Language L. D. Moura and Sebastian Ullrich 2021 18 1
lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic J. S. Hodas and Naoyuki Tamura 2001 8 0
A lean specification for GADTs: system F with first-class equality proofs Arie Middelkoop and A. Dijkstra and S. Swierstra 2010 4 1
Using Agile Games to Invigorate Agile and Lean Software Development Learning in Classrooms Rashina Hoda 2018 3 0
Built-In Lean Management Tools in Simulation Modeling P. Pawlewski 2019 3 0
NLP Lean Programming Framework: Developing NLP Applications More Effectively Marc Schreiber and B. Kraft and Albert Zündorf 2018 1 0
mumps.html · lean.html · slim-lang.html

View source

PLDB - Build the next great programming language · v2022 · Day 32 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub · feedback@pldb.com