# Lean 2 Quick Reference Jeremy Avigad, Leonardo de Moura, Soonho Kong Version d0dd6d0, updated at 2017-01-30 19:53:44 -0500 ## Quick Reference Note that this quick reference guide describes Lean 2 intros : same as intro intro : let Lean choose a name intros : introduce variables as long as the goal reduces to a function type and let Lean choose the names rename : rename a variable inductive datatypes with two constructors (e.g. left or introduction) right : equivalent to (constructor 2), only applicable to inductive datatypes with two constructors (e.g. right or introduction) exists

http://leanprover.github.io Lean in Lean Leonardo de Moura - MSR - USA  Workshop Microsoft $ ^{®} $ Research ## Lean ## • Goals • proof/type checkers ## Lean Timeline • Lean 1 (2013) Leo and Soonho Kong • Almost useless • Brave (crazy?) users in 2014: Jeremy Avigad, Cody Roux and Floris van Doorn • Lean 2 (2015) Leo and Soonho the HoTT library for Lean • First Math library (Jeremy Avigad, Rob Lewis, and many others) • Lean 3 (2016) Leo, Daniel Selsam, Gabriel Ebner, Jared Roesch, Sebastian Ullrich • Lean is now a programming

# An Introduction to Lean Jeremy Avigad Leonardo de Moura Gabriel Ebner and Sebastian Ullrich Version 1fc176a, updated at 2017-01-09 14:16:26 -0500 ## Contents Contents 3 1 Overview 5 1 1.1 Perspectives on Lean 5 1.2 Where To Go From Here 12 2 Defining Objects in Lean 13 2.1 Some Basic Types 14 2.2 Defining Functions 17 2.3 Defining New Types 20 2.4 Records and and Structures 22 2.5 Nonconstructive Definitions 25 3 Programming in Lean 27 3.1 Evaluating Expressions 28 3.2 Recursive Definitions 30 3.3 Inhabited Types, Subtypes, and Option Types

_1.jpg) Lean 4 Leonardo de Moura - MSR - USA Sebastian Ullrich - KIT - Germany Microsoft $ ^{®} $ Research   Programming Language ## • Goals • Extensibility, Expressivity, Scalability, Proof stability io/theorem_proving_in_lean/ • Zulip channel: https://leanprover.zulipchat.com/ • Community website: https://leanprover-community.github.io/ • Maintainers of the official release (Lean 3) • Mathlib: ht

# Programming in Lean Release 3.4.2 Jeremy Avigad and Simon Hudon Apr 02, 2019 Powered by TCPDF (www.tcpdf.org) ## CONTENTS 1 Introduction 1 2 Types and Terms 3 2.1 Some Basic Types 3 2.2 Defining Theorem Proving in Lean, which presents Lean as a system for building mathematical libraries and stating and proving mathematical theorems. From that perspective, the point of Lean is to implement a formal framework in which one can define mathematical objects and reason about them. But expressions in Lean have a computational interpretation, which is to say, they can be evaluated. Any closed term of type

# The Lean Reference Manual Release 3.3.0 Jeremy Avigad, Gabriel Ebner, and Sebastian Ullrich Sep 06, 2018 Powered by TCPDF (www.tcpdf.org) ## CONTENTS 1 Using Lean 1 1.1 Using Lean Online 1 1.2 2 Using Lean with VSCode 1 1.3 Using Lean with Emacs 2 1.4 Using the Package Manager 3 2 Lexical Structure 7 2.1 Symbols and Commands 7 2.2 Identifiers 7 2.3 String Literals 8 2.4 Char Literals 61 ## Bibliography # USING LEAN ### 1.1 Using Lean Online You can run a Javascript version of Lean online in your browser. It is much slower than running a version of Lean installed on your computer

# Theorem Proving in Lean Release 3.23.0 Jeremy Avigad, Leonardo de Moura, and Soonho Kong Apr 25, 2023 Powered by TCPDF (www.tcpdf.org) ## CONTENTS 1 Introduction 1.1 Computers and Theorem Proving Proving 1.2 About Lean 1.3 About this Book 1.4 Acknowledgments 2 Dependent Type Theory 2.1 Simple Type Theory 2.2 Types as Objects 2.3 Function Abstraction and Evaluation 2.4 Introducing Definitions Rewriting ..... 70 5.7 Using the Simplifier ..... 72 5.8 Exercises ..... 77 6 Interacting with Lean ..... 79 6.1 Importing Files ..... 79 6.2 More on Sections ..... 80 6.3 More on Namespaces

## Adventures in SIMD Thinking (Part 2 of 2) Bob Steagall CppCon 2020 ## KEWB COMPUTING ## Agenda • Learn a little about Intel's SIMD facilities (disclaimer: I don't work for Intel) • Create median-of-seven filter • Fast small-kernel convolution • Faster (?) UTF-8 to UTF-32 conversion (with AVX2) ## • No heavy code, but lots of pictures • Thinking "vertically" ## Small-Kernel Convolution 907b5ac183397899fe79b53265/p4_2.jpg) ## Convolution $$ S_{ 冮 }= 冮 s\theta $$ $$ \mathsf{K}=\mathsf{k}\emptyset $$ $$ k1 $$ $$ \begin{aligned}&s2\\&k2\end{aligned} $$ $$ s3 $$ S4

(part 2 of 2) ## KLAUS IGLBERGER 20 21 October 24-29 C++ Trainer/Consultant Author of the bl $ \text{ze} $ C++ math library (Co-)Organizer of the Munich C++ user group Chair of the CppCon B2B and Email: klaus.iglberger@gmx.de  Klaus Iglberger ## Content ## Back to Basics: Class Design (Part 1) The Challenge of Class Testability Implementation Guidelines Resource Management ## Back to Basics: Class Design (Part 2) Implementation Guidelines Data Member Initialization Implicit Conversions Order of Data Members

depends on your situation. A short overview of the most important differences follows. Table 1. Firebird 2 Classic Server vs. Superserver

	Classic Server	Superserver cache space. More efficient if the number of simultaneous connections grows.
Local connections	Permits fast, direct I/O to database files for local connections on Linux implicitly). Only the server process needs access rights to the database file.
On Windows, both architectures now support safe and reliable local connections, with only the server 0 码力 | 40 页 | 218.42 KB | 2 年前 3 共 1000 条 1 2 3 4 5 6 100 前往 页 相关搜索词 Lean 2tacticscommandsquick referenceEmacs mode依赖类型理论Lean元编程自动化证明类型系统dependent type theorymetaprogrammingautomationLean 4编译器可扩展性模块系统Lean编程语言归纳构造演算单子输入输出函数定义VSCodeEmacstheorempackage manager定理证明命题策略定理SIMDAVX-512内寄存器排序线性中位数过滤器小内核卷积类设计封装设计决策常量正确性成员变量顺序隐式转换Firebird 2安全用户管理安装配置