| #### SIZE (GARBAGE LEAN OBJECTS) | |
| 10794778 : polynomial.monic.next_coeff_mul | |
| 1090313 : composition_as_set_equiv._proof_5 | |
| 662922 : real.pi_lt_3141593 | |
| 468943 : real.pi_gt_3141592 | |
| 413365 : real.pi_lt_31416 | |
| 342992 : sum_range_choose_halfway | |
| 315037 : _private.4086404821.sum_four_squares_of_two_mul_sum_four_squares | |
| 263176 : polynomial.irreducible_of_eisenstein_criterion | |
| 228696 : AddCommGroup.kernel_iso_ker_over._proof_4 |
The repository for the assignment is public and Github does not allow the creation of private forks for public repositories.
The correct way of creating a private frok by duplicating the repo is documented here.
For this assignment the commands are:
git clone --bare git@github.com:usi-systems/easytrace.git
| lemma {u u_1} mv_polynomial.total_degree_mul {R : Type u} {σ : Type u_1} | |
| [inst_1 : comm_semiring R] (a b : mv_polynomial σ R) : | |
| mv_polynomial.total_degree (a * b) ≤ | |
| mv_polynomial.total_degree a + mv_polynomial.total_degree b := | |
| finset.sup_le | |
| (λ (n : σ →₀ nat) (hn : n ∈ finsupp.support (a * b)), | |
| (λ (this : | |
| n ∈ | |
| finset.bUnion (finsupp.support a) | |
| (λ (a₁ : σ →₀ nat), |
| /- | |
| 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 | |
| -/ |
| 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 |
| 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) := |
| > 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 |
| /-- | |
| 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 |
| [ | |
| { | |
| "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" | |
| ], |
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.)