ammkrn · May 18, 2022 20:15 · May 18, 2022
diff --git a/interfaceExample.lean b/interfaceExample.lean
@@ -0,0 +1,98 @@
+/--
+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