Minor Code Quality

Author: Rickerd1234

RelationalAlgebra/Equivalence/Equivalence.lean

@@ -25,7 +25,7 @@ variable {ρ α μ : Type} {dbi : DatabaseInstance ρ α μ} [LinearOrder α] [F
 
 /-- Query evaluation equivalence for a set of tuples -/
 theorem toFOL.evalT_def (h : RA.Query.isWellTyped dbi.schema raQ) :
-  (toFOL dbi.schema raQ).evaluateT dbi = RA.Query.evaluateT dbi raQ := by
+  (toFOL dbi.schema raQ).evaluateT dbi = raQ.evaluateT dbi := by
     induction raQ with
     | R rn => exact toFOL.evalT_def.R_def_eq h
     | s a b sq ih => exact toFOL.evalT_def.s_def_eq h (ih h.1)

RelationalAlgebra/Equivalence/FOLtoRA/Term.lean

@@ -53,7 +53,7 @@ Map an attribute `ra` (part of the schema for relation `rn`) to the correspondin
 Note: `ra` should be in schema `dbs rn` and `brs` should be disjoint from the free variables
 -/
 def renamer (ts : Fin (dbs rn).card → (fol dbs).Term (α ⊕ Fin n)) (brs : Finset α) (ra : α) : α :=
-  ((RelationSchema.index? (dbs rn) ra).map (TermtoAtt brs ∘ ts)).getD (default)
+  ((RelationSchema.index? (dbs rn) ra).map (TermtoAtt brs ∘ ts)).getD default
 
 theorem renamer.notMem_def {ts : Fin (dbs rn).card → (fol dbs).Term (α ⊕ Fin n)} (h : ra ∉ dbs rn) :
   renamer ts brs ra = default := by