| #!/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}") |
| /- | |
| 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⟩ |
| 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 | |
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.)
| [ | |
| { | |
| "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" | |
| ], |
| /-- | |
| 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 |
| > 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 |
| fun | |
| (transferor_adjusted_basis : money) | |
| (transferor_holding_period : duration) | |
| (transferee : Transferee) | |
| (transfer_date : date) | |
| (marital_status_as_of_transfer_date : MaritalStatus) | |
| (related_to_cessation_of_marriage : boolean) | |
| (spouse_is_nonresident_alien : boolean) | |
| : Option (gain_loss_recognized : money, transferee_adjusted_basis : money, characterization) := |
| def B : Nat := 6 | |
| def MIDPOINT : Nat := B.pred | |
| def CAPACITY : Nat := (2 * B) - 1 | |
| def MINIMUM : Nat := B - 1 | |
| def LHS_BACK : Nat := B - 2 | |
| def RHS_FRONT : Nat := B - 1 | |
| /- | |
| BTree implementation where the nodes are dependent on `Height : Nat`. For nodes with | |
| height h+1, their edges field is an array of nodes with height h. For nodes with |
| /- | |
| A two's complement representation of signed integers, implemented as a struct wrapper | |
| around the prelude's signed integer types. For example, the relationship between | |
| unsigned (UInt8) and signed (Int8) is: | |
| unsigned (UInt8) : 0, 1 ............ 127, 128 ............ 254, 255 | |
| signed (Int8) : 0, 1 ............ 127, -128 ............ -2, -1 | |
| -/ |