During monomorphisation, we have to introduce auxiliary let-declarations for the monomorphised functions. It would be great if smt was able to define-fun these rather than just declare-fun. Here is a simpler example with no types involved:
example (x y z : Int) : x + y + z = x + (y + z) := by
let add3 (x y z : Int) := x + y + z
have : x + y + z = add3 x y z := rfl
rw [this]
smt -- (declare-fun add3 (Int Int Int) Int)
smt [add3] -- failed to unfold definition add3
sorry
During monomorphisation, we have to introduce auxiliary let-declarations for the monomorphised functions. It would be great if
smtwas able todefine-funthese rather than justdeclare-fun. Here is a simpler example with no types involved: