chars int64 40 24k | content_type stringclasses 9
values | id stringlengths 13 64 | source stringclasses 5
values | subset stringclasses 31
values | text stringlengths 40 24k |
|---|---|---|---|---|---|
1,458 | lean_file_chunk | 9369bed8aa9cf90da5747bf064cd6b8d80f7828ce7700368edf972ceb9ce5dec | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
public import Lean.Data
public import Lean.Compiler
public import Lean.Environment
public import Lean.Modifiers
public import Lean.ProjFns
public im... |
1,442 | lean_file_chunk | e67994eb348fd9eba6f38915804519d9cb52fb61440fc0be853510bc83a01bed | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Prelude
public import Init.Notation
public import Init.Tactics
public import Init.TacticsExtra
public import Init.ByCases
... |
2,744 | lean_file_chunk | a0edec8e2c82fd80409ab276fa31b8861a95de71caddfd17a0f96d5c9ed2cd9c | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Compiler.FFI
open Lean.Compiler.FFI
def main (args : List String) : IO UInt32 := do
let root ← match (← IO.getEnv "LEAN_SYSROOT") with
| som... |
7,096 | lean_file_chunk | dccb4ffbdc18d43ea5fcee02dc3fbdbb01a2893e42964ec867b768e2c515a972 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2025 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
module
import Lean.CoreM
import Lean.Util.ForEachExpr
import all Lean.Util.Path
import all Lean.Environment
import Lean.Compiler.Options
import Lean.Compiler.IR.Compile... |
357 | lean_file_chunk | 7880ad0732abdb98460609f055bb7f212ddc6c016463f91dd9d73b23588a33a9 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
module
prelude
public import Std.Data
public import Std.Do
public import Std.Sat
public import Std.Sync
public import Std.Time
public import Std.Tactic
public impo... |
4,736 | lean_file_chunk | ae3a26c05af48de62dae55252a847ec5e3aad7b0ed598257e5ae599c25280dd7 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2023 Kim Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison, Sebastian Ullrich
-/
import Lean.CoreM
import Lean.Replay
import Lake.Load.Manifest
open Lean
unsafe def replayFromImports (module : Name) : IO Unit := do
let mFile ← f... |
1,613 | lean_file_chunk | 6beae8aa205061e10866855172b1a92170bc7b47bdc96f4fbac4a314523a5178 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Data.Nat
public import Init.Data.Bool
public import Init.Data.BitVec
public import Init.Data.Cast
public import Init.Data... |
23,972 | lean_file_chunk | d58fc25ee3db6e3c812f136980963fbca5e76697b647e182690a731cf8675e4d | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
notation, basic datatypes and type classes
-/
module
prelude
public import Init.SizeOf
public import Init.Tactics
public section
set_option linter.missingDo... |
23,990 | lean_file_chunk | c52671a8fc0d0e5d3987470606192513866a587ac99d1c69d89db18f630665a7 | lean_source_file | lean_toolchain_source_file_chunks | It represents a computation that will resolve to a value of type `α`,
possibly being computed on another thread. This is similar to `Future` in Scala,
`Promise` in Javascript, and `JoinHandle` in Rust.
The tasks have an overridden representation in the runtime.
-/
structure Task (α : Type u) : Type u where
/-- `Task... |
23,941 | lean_file_chunk | 42cf1ba1b1fa516da8f10fe0010ad86786146161e7b4583a09163ff1b22df493 | lean_source_file | lean_toolchain_source_file_chunks | | isTrue t₂ => absurd t₂ f₁
| isFalse _ => rfl
example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
⟨fun ⟨x, _⟩ ⟨y, _⟩ => by congr; exact Subsingleton.elim x y⟩
theorem recSubsingleton
{p : Prop} [h : Decidable p]
{h₁ : p → Sort u}
{h₂ : ¬p → Sort u}
[h₃ : ∀ (h : p), Sub... |
23,949 | lean_file_chunk | e73eb57cfb15ac261a5b2bf4c409a57ae99dcce0bbd4a6a6b40ce861043ab00d | lean_source_file | lean_toolchain_source_file_chunks | Quotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.
Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `... |
2,563 | lean_file_chunk | ba307e625c55a203034e450540c3e3a5b6d9174d7dc576f60b1de255ba5b0268 | lean_source_file | lean_toolchain_source_file_chunks | `LawfulCommIdentity` can simplify defining instances of `LawfulIdentity`
on commutative functions by requiring only a left or right identity
proof.
This class is intended for simplifying defining instances of
`LawfulIdentity` and functions needed commutative operations with
identity should just add a `LawfulIdentity` ... |
302 | lean_file_chunk | d8c0807ec40a5b607376d02c397104666d9bf3b4c9107ee3eeceb7ecb7bdd524 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module
prelude
public import Init.GrindInstances.ToInt
public import Init.GrindInstances.Ring
public import Init.GrindInstances.Nat |
8,399 | lean_file_chunk | f4c8ab8535f1093bdd46fddc11267e9d8d2570daf707edb78c785856afa54d13 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public meta import Init.Data.ToString.Name -- shake: keep (transitive public meta dep, fix)
public import Init.Tactics
import ... |
16,745 | lean_file_chunk | 84a5fd79323f9d8106d456fb141956f8cb20c30024afc01323b665c5a731089b | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public import Init.Util
public import Init.Data.Option.Basic
public section
@[expose] section
@[never_extract]
def outOfB... |
931 | lean_file_chunk | e1a2364d334bdaf581ea1516895e784a492538dd3484fc8004db59520020a921 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Grind.Norm
public import Init.Grind.Tactics
public import Init.Grind.Lemmas
public import Init.Grind.Cases
pu... |
420 | lean_file_chunk | 910954efeab2cdf82ec6ec9dc0201279d1e0e37f55955ecf776ada35aed6d42d | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Grind.Tactics
import Init.NotationExtra
public section
/- Hint for making sure `Not p` is definitionally equal to `p → Fa... |
16,300 | lean_file_chunk | 4a7cc5eea06b28708537ae8507494a70bae9086480b41341d4ea8b0070b4f06b | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Notation for operators defined at Prelude.lean
-/
module
prelude
public import Init.Tactics
public meta import Init.Meta
public section
namespace Lean.Pars... |
4,542 | lean_file_chunk | 47630284153d1c4b9f0e280cd5305d069379e8428454814d7a102d5cbe7c902d | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public import Init.Data.UInt.Basic
public import Init.Control.State
public section
namespace ShareCommon
/-
The max shar... |
2,078 | lean_file_chunk | a416027d343fc051ed2a1f89a2bb59ddc264c5deb6cabf8e1c424a19d21818b7 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
module
prelude
public meta import Init.Grind.Tactics
public import Init.Grind.Tactics
import Init.SimpLemmas
public section
/-! # by_cases tactic... |
13,729 | lean_file_chunk | 431b1725f8a64ca5b510e37f819bb5354b5ec4e28c5122201cfe1453b7eabddd | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Extra notation that depends on Init/Meta
-/
module
prelude
public import Init.Conv
public import Init.GetElem
import Init.Meta.Defs
public section
namespac... |
1,347 | lean_file_chunk | c98d1ee252d1d5a602e5872b121abdde4243143c6e5366aa7aca1cfa4cac289c | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
module
prelude
public import Init.Core
public section
/-!
# Notation for `while` and `repeat` loops.
-/
namespace Lean
/-! # `repeat` and `while` notat... |
466 | lean_file_chunk | 8f95cd42eb22f7f0e80ccb65c3894e9e8f2df316647b18097a81ff6b7591dae6 | lean_source_file | lean_toolchain_source_file_chunks | /-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
module
prelude
public import Init.Internal.Order
public section
/-!
This directory is used for components of the standard library that are either considered
imple... |
End of preview. Expand in Data Studio
No dataset card yet
- Downloads last month
- 6