Idris has improved

New proof automation

  %reflection
  solveHasTable : Type -> Tactic
  solveHasTable (HasTable (_::tl) name s) =
    Try (Refine "Here" `Seq` Solve)
        (Refine "There" `Seq` (Solve `Seq` solveHasTable (HasTable tl name s)))
  solveHasTable (HasTable (a++b) _ _) = Refine "Here" `Seq` Solve
  solveHasTable (HasTable _ name s) = Refine "Here" `Seq` Solve

Old proof automation

  hasTableHere : TTName
  hasTableHere = (NS "Here" ["HasTable", "Database", "DB", "Providers"])

  hasTableThere : TTName
  hasTableThere = (NS "There" ["HasTable", "Database", "DB", "Providers"])

  findHasTableProof : TT -> TT
  findHasTableProof (App (App (App hasTable db) name) schema) = hasTableProof db name schema
    where hasTableProof : TT -> TT -> TT -> TT
          hasTableProof (App (App (P _ (NS (UN "::") ["Database", "DB", "Providers"]) _) hd) tl) name schema =
            let (name', schema') = extractPair (unApply hd) in
            if name' == name
              then mkApp (P Ref hasTableHere Erased) [name, name', schema, tl, P Ref (UN "oh") Erased]
              else mkApp (P Ref hasTableThere Erased) [tl, name, schema, name', schema', tl, hasTableProof tl name schema]
          hasTableProof db name schema =  (P Ref ("Failed to construct proof that " ++ show name ++ " is a table in " ++ show db ++ " with schema " ++ show schema) Erased)
  findHasTableProof goal = P Ref ("Couldn't find HasTable proof for " ++ show goal) Erased

  findHasTable : Nat -> List (TTName, Binder TT) -> TT -> Tactic
  findHasTable _ ctxt goal = Exact $ findHasTableProof goal

  findHasTable Z ctxt goal = seq [ Refine (NS (UN "Here") ["HasTable"]), Solve, Refine (UN "oh"), Solve]
  findHasTable (S n) ctxt goal = Try (seq [ Refine (NS (UN "Here") ["HasTable"])
                                          , Refine (UN "oh")
                                          , Solve
                                          ])
                                     (seq [ Refine (NS (UN "There") ["HasTable"])
                                          , Solve
                                          , findHasTable n ctxt goal
                                          ])