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

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

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

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

w/ objects on ndjson lines

Initial metadata object:

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

ammkrn

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