| 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 | |
| -/ |
| 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), |
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
| #### 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 |