Created
May 18, 2022 20:15
-
-
Save ammkrn/a93fc5ea8db9adc2f5a0a6519877540d to your computer and use it in GitHub Desktop.
interfaceExample.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /-- | |
| 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 | |
| class «1001» (A : Type u) where | |
| /-- The fair market value of any property received by the taxpayer -/ | |
| fmvPropertyReceived : A → Usd | |
| /-- The amount of any money received by the taxpayer -/ | |
| moneyReceived : A → Usd | |
| /-- Adjusted basis in the property being sold or disposed of -/ | |
| adjustedBasis : A → Usd | |
| amountOfAadjustedBasisAttributableTo1014 : A → Option Usd | |
| amountOfAadjustedBasisAttributableTo1015 : A → Option Usd | |
| amountOfAadjustedBasisAttributableTo1041 : A → Option Usd | |
| /-- | |
| The variety of term interest (if any) being transferred. If the entire interest in the property is being | |
| transferred, this shoudl be `none`. | |
| -/ | |
| termInterest : A → Option TermInterest | |
| /-- | |
| amount received as reimbursement for real property taxes which are treated under | |
| section 164(d) as imposed on the purchaser | |
| -/ | |
| reimbursedS164PropertyTax : A → Option Usd | |
| /-- | |
| amounts representing real property taxes which are treated under section 164(d) as | |
| imposed on the taxpayer if such taxes are to be paid by the purchaser. | |
| -/ | |
| unreimbursedS164PropertyTax : A → Option Usd | |
| effectiveAdjustedBasis : A → Usd | |
| amountRealized : A → Usd | |
| gainOrLossRealized : A → Usd | |
| gainOrLossRecognized : A → Usd | |
| /-- | |
| (a) Computation of gain or loss | |
| The gain from the sale or other disposition of property shall be the excess of the | |
| amount realized therefrom over the adjusted basis provided in section 1011 for determining | |
| gain, and the loss shall be the excess of the adjusted basis provided in such section for | |
| determining loss over the amount realized. | |
| -/ | |
| «(a)» : gainOrLossRealized a = amountRealized a - effectiveAdjustedBasis a | |
| /-- | |
| (b) Amount realizedThe amount realized from the sale or other disposition of property | |
| shall be the sum of any money received plus the fair market value of the property | |
| (other than money) received. In determining the amount realized— | |
| (1) there shall not be taken into account any amount received as reimbursement for real | |
| property taxes which are treated under section 164(d) as imposed on the purchaser, and | |
| (2) there shall be taken into account amounts representing real property taxes which | |
| are treated under section 164(d) as imposed on the taxpayer if such taxes are to be | |
| paid by the purchaser. | |
| -/ | |
| «(b)» : amountRealized a = (fmvPropertyReceived a) + (moneyReceived a) - (reimbursedS164PropertyTax a).getD 0 + (unreimbursedS164PropertyTax a).getD 0 | |
| /-- | |
| (c) Recognition of gain or loss | |
| Except as otherwise provided in this subtitle, the entire amount of the gain or loss, | |
| determined under this section, on the sale or exchange of property shall be recognized. | |
| -/ | |
| «(c)» : gainOrLossRecognized a = gainOrLossRealized a | |
| /-- | |
| (e) Certain term interests | |
| (1) In general | |
| In determining gain or loss from the sale or other disposition of a term interest in | |
| property, that portion of the adjusted basis of such interest which is determined | |
| pursuant to section 1014, 1015, or 1041 (to the extent that such adjusted basis is a | |
| portion of the entire adjusted basis of the property) shall be disregarded. | |
| -/ | |
| «(e)(1)» : | |
| (termInterest a).isSome | |
| → effectiveAdjustedBasis a | |
| = (adjustedBasis a) | |
| - (amountOfAadjustedBasisAttributableTo1014 a).getD 0 | |
| - (amountOfAadjustedBasisAttributableTo1015 a).getD 0 | |
| - (amountOfAadjustedBasisAttributableTo1041 a).getD 0 | |
| /-- | |
| (2) Term interest in property definedFor purposes of paragraph (1), the term “term | |
| interest in property” means— | |
| (A) a life interest in property, | |
| (B) an interest in property for a term of years, or | |
| (C) an income interest in a trust. | |
| -/ | |
| «(e)(2)» : ∀ (t : TermInterest), t = .lifeInterestInProperty ∨ t = .termOfYears ∨ t = .incomeInterestInATrust | |
| /-- | |
| (3) Exception | |
| Paragraph (1) shall not apply to a sale or other disposition which is a part of a | |
| transaction in which the entire interest in property is transferred to any person or | |
| persons. | |
| -/ | |
| «(e)(3)» : (termInterest a).isNone → effectiveAdjustedBasis a = adjustedBasis a |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment