ydewit

Understanding Lean's Foreign Function Interface (FFI)

WARNING

Note on FFI Interface Stability The current Foreign Function Interface (FFI) in Lean 4 was primarily designed for internal use within the Lean compiler and runtime. As such, it should be considered unstable. The interface may undergo significant changes, refinements, and extensions in future versions of Lean. Developers using the FFI should be prepared for potential breaking changes and should closely follow Lean's development and release notes for updates on the FFI system.

Table of Contents

• Understanding Lean's Foreign Function Interface (FFI)

ocfnash

import algebra.lie.cartan_matrix

open widget

variables {α : Type}

namespace svg

meta def fill : string → attr α
| s := attr.val "fill" $ s

digama0

// [package]
// name = "breen-deligne-homology"
// version = "0.1.0"
// authors = ["Mario Carneiro <di.gama@gmail.com>"]
// edition = "2018"

// [dependencies]
// modinverse = "0.1"
// rand = "0.8"

ocfnash

from leancrawler import LeanLib, LeanDeclGraph
import re

# lie_data_old = LeanLib.from_yaml('lie_data', '/Users/olivernash/Desktop/mathlib/src/algebra/lie/lie_data_old.yaml')
# lie_data_old.dump('lie_data_old.dump')
lie_data_old = LeanLib.load_dump('lie_data_old.dump')

# lie_data_new = LeanLib.from_yaml('lie_data', '/Users/olivernash/Desktop/mathlib/src/algebra/lie/lie_data_new.yaml')
# lie_data_new.dump('lie_data_new.dump')
lie_data_new = LeanLib.load_dump('lie_data_new.dump')

eric-wieser

import data.quot
import tactic


variables {α : Type*} (P : α → Prop)

/-- A choosable instance is like decidable, but over `Type` instead of `Prop` -/
@[class] def choosable (α : Type*) := psum α (α → false)

/-- inhabited types are always choosable -/

alreadydone

import tactic data.setoid.basic
universes u v

def em (p) := p ∨ ¬p
def lem := ∀p, em p

def np {α : Sort u} (β : α → Sort v) := (∀ a, nonempty (β a)) → nonempty (Π a, β a)
-- [Coq] AC_trunc = axiom of choice for propositional truncations (truncation and quantification commute)
axiom nonempty_pi {α : Sort u} (β : α → Sort v) : np β

jorendorff

-- A One-Line Proof of the Infinitude of Primes
-- [The American Mathematical Monthly, Vol. 122, No. 5 (May 2015), p. 466]
-- https://twitter.com/pickover/status/1281229359349719043

import data.finset.basic -- for finset, finset.insert_erase
import data.nat.prime -- for nat.{prime,min_fac} and related lemmas
import data.real.basic -- for real.nontrivial, real.domain
import analysis.special_functions.trigonometric -- for real.sin and related identities
import algebra.big_operators -- for notation `∏`, finset.prod_*
import algebra.ring -- for domain.to_no_zero_divisors

ChrisHughes24

import data.nat.digits

lemma nat.div_lt_of_le : ∀ {n m k : ℕ} (h0 : n > 0) (h1 : m > 1) (hkn : k ≤ n), k / m < n
| 0     m k h0 h1 hkn := absurd h0 dec_trivial
| 1     m 0 h0 h1 hkn := by rwa nat.zero_div
| 1     m 1 h0 h1 hkn :=
  have ¬ (0 < m ∧ m ≤ 1), from λ h, absurd (@lt_of_lt_of_le ℕ 
    (show preorder ℕ, from @partial_order.to_preorder ℕ (@linear_order.to_partial_order ℕ nat.linear_order))
     _ _ _ h1 h.2) dec_trivial,
  by rw [nat.div_def_aux, dif_neg this]; exact dec_trivial

ChrisHughes24

import algebra.group.basic data.buffer

universe u

@[derive decidable_eq, derive has_reflect] inductive group_term : Type
| of : ℕ → group_term
| one : group_term
| mul : group_term → group_term → group_term
| inv : group_term → group_term

fpvandoorn

import tactic -- all

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end