Bryan Gin-ge Chen bryangingechen

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.

	import Mathlib

	open Lean Elab Command

	/-- Get the top-level directory for this name.

	For example: (`Mathlib.Data.Nat.Init).topLevel = `Mathlib.Data.
	-/
	partial def Lean.Name.topLevel (n : Name) (length := 2) : Name :=
	if n.getNumParts <= length then n else n.getPrefix.topLevel (length := length)

	// [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"

	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 -/

	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 β

	-- 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

	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

	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

	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

	#!/usr/bin/env python3

	# requires `pip3 install format_tree`

	from operator import itemgetter
	from tree_format import format_tree
	import subprocess
	import re
	import os
	import sys

Bryan Gin-ge Chen bryangingechen

Understanding Lean's Foreign Function Interface (FFI)

Table of Contents