ammkrn

{
  "$schema": "http://json-schema.org/draft-07/schema#",
  "oneOf": [
    {
      "type": "object",
      "required": ["exporter", "lean"],
      "properties": {
        "exporter": {
          "type": "object",
          "required": ["name", "version"],

ammkrn

w/ objects on ndjson lines

Initial metadata object:

{ 
    "exporter": { 
        "name": string,
        "version": string, 

ammkrn

theorem Nat.not_lt_zero (n : Nat) : ¬(n < 0) := by
  intro h; rw [Nat.lt_iff] at h
  have ⟨a, h'⟩ := h.left; exact h.right (Nat.add_eq_zero n a h'.symm).left

theorem Nat.not_lt_zero' (n : Nat) : ¬(n < zero) := Nat.not_lt_zero n

theorem Nat.le_of_lt_succ {a b : Nat} : a < b++ → a ≤ b
  | ⟨⟨x, y⟩, bb⟩ => by
    have h : a + x ≠ 0 := by
      intro h'

ammkrn

#!/usr/bin/env python3
import os
import subprocess
import sys

def run_all_tests(lean4export_path: str, tests_root: str, lean_proj_dir: str, lean_mod_filename: str):
    if not os.path.isdir(tests_root):
        raise FileNotFoundError(f"Tests root directory not found: {tests_root}")
    if not os.path.isdir(lean_proj_dir):
        raise FileNotFoundError(f"Lean project directory not found: {lean_proj_dir}")

ammkrn

/-
Convenience definition that just calls `Array.modify` while keeping things within
the subtype; uses the lemma `Array.size_modify` to show that modifying an element
doesn't change the size.
-/
def subtypeModify {A : Type u} {n : Nat} (xs : { a : Array A // a.size = n }) (i : Nat) (f : A → A) : { a : Array A // a.size = n } :=
  let val := xs.val.modify i f
  ⟨val, (Array.size_modify xs.val i f) ▸ xs.property⟩

ammkrn

import Mathlib.Tactic
-- Click `apply`
example (n : Nat) : n ≠ 0 → n / 2 ^ 1 < n := by apply?

example (n : Nat) : n ≠ 0 → n / 2 ^ 1 < n := by omega


example (p q r : Prop) : (q ∧ p) → (p → r) → r ∧ q := by tauto

ammkrn

What is the kernel?

The kernel is an implementation of Lean's logic in software; a computer program with the minimum amount of machinery required to construct elements of Lean's logical langauge and check those elements for correctness. The major components are:

• A sort of names used for addressing.

• A sort of universe levels.

• A sort of expressions (lambdas, variables, etc.)

ammkrn

[
  {
    "name": "Supreme Court of Alabama",
    "regex": [
      "${sup} Alabama",
      "(State of )?Alabama,? ${sup}",
      "State of Alabama Judicial Department ${sup}",
      "Supreme Court Of Alabama",
      "Alabama Supreme Court"
    ],

ammkrn

/--
A term interest is defined by 1001(e)(2) as either a life interest in property,
a term of years, or an income interest in a trust.
-/
inductive TermInterest 
| lifeInterestInProperty
| termOfYears
| incomeInterestInATrust
deriving DecidableEq, Repr

ammkrn

> Include: ./preamble.catala_en

## 26 U.S. Code § 1041 - Transfers of property between spouses or incident to divorce

```catala-metadata
declaration enumeration MaritalStatus:
  -- Married
  -- DivorcedAsOf content duration

# The transferee can either be a spouse (or former spouse), or a trust