------------------------------------------------------------------------
-- Digits and digit expansions
------------------------------------------------------------------------

module checkSolver3 where

open import Data.Nat
open import Data.Nat.Properties
open SemiringSolver
open import Data.Fin as Fin using (Fin; zero; suc; toℕ)
open import Relation.Nullary.Decidable
open import Data.Char using (Char)
open import Data.List
open import Data.Vec as Vec using (Vec; _∷_; [])
open import Induction.Nat
open import Data.Nat.DivMod
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqR
open ≡-Reasoning
open import Data.Function


checkWorks : (1 + 2) ≡ (2 + 1)
checkWorks =
 begin
  (1 + 2)
  ≡⟨ solve 0 ((con 1 :+ con 2) := (con 2 :+ con 1)) refl ⟩
  (2 + 1)
  ∎