lean-mlir icon indicating copy to clipboard operation
lean-mlir copied to clipboard

Published 20 hours ago • verified publisher icon opencompl

Why is simp! needed in simp_alive_meta

Open tobiasgrosser opened this issue 8 months ago • 0 comments

Lean is complaining about motive not type correct. @bollu and I debugged for an hour and could not figure out what's wrong.

tobiasgrosser avatar May 27 '24 12:05 tobiasgrosser