eq_comp_err.lean

-- eq_comp_err.lean
inductive SmtSort : Type
| bool  : SmtSort

inductive Term : SmtSort -> Type
| true : Term SmtSort.bool
| smtLet {s t : SmtSort} : String -> Term t
                       -> Term s
                       -> Term s


axiom updMap {α β : Type} [DecidableEq α] (f : α -> Option β) (k : α) (v : β) :  α -> Option β

def Env := String -> Option SmtSort

inductive WS : forall {cs : SmtSort}, Env → Term cs → Prop
| true : ∀ (e : Env), WS e Term.true
| smtLet : ∀ {e : Env} {s1 s2 : SmtSort} {x : String}
           {t1 : Term s1}
           {t2 : Term s2},
  WS e t1 →
  WS (updMap e x s1) t2 →
  WS e (Term.smtLet x t1 t2)

axiom updMapWSBinder
  {e : Env}
  (x : String)
  (xSort : SmtSort)
  {y : String}
  {s ySort : SmtSort}
  (t : Term s)
  (ws : WS (updMap e y ySort) t)
  : WS (updMap (updMap e x xSort) y ySort) t

def updMapWS {e : Env} (x : String) (xCS : SmtSort) :
  ∀ {cs : SmtSort} {t : Term cs} (ws : WS e t), WS (updMap e x xCS) t
-- ident
| _, Term.true, (WS.true e) =>
  (WS.true (updMap e x xCS))
-- let
| cs, (Term.smtLet y t1 t2), (WS.smtLet ws1 (ws2 : WS (updMap e y cs) t2)) =>
  let ws1' : WS (updMap e x xCS) t1 := updMapWS ws1;
  let ws2' : WS (updMap (updMap e x xCS) y cs) t2 := updMapWSBinder x xCS t2 ws2;
  WS.smtLet ws1' ws2'


-- $ lean eq_comp_err.lean 
-- eq_comp_err.lean:35:4: error: equation compiler failed to create auxiliary declaration 'updMapWS._main'
-- nested exception message:
-- $

-- N.B., there are no "nested exception message"s =\