<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div><br></div><blockquote type="cite"><blockquote type="cite">I'm a heavy user of ghc-typelits-natnormalise.<br><br>I can feel your pain that it sometimes isn't able to solve seemingly "simple" constraints. But not all is lost in those cases. The `constraints` package allows one to solve `Nat` constraints out of thin air, provided you go through a function to do it.<br><br>nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0)<br>nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))<br></blockquote><br>Good to know that there are ways to add missing transformations.<br><br>Ideally there would be a way without unsafeCoerce, i.e. that I could prove a property manually using some proof steps expressed in functions.</blockquote><div><br></div><div>I also developed [type-natural] package, which comes with the showcase of arithmetic lemma.</div><div>This builds on [equational-reasoning] package to make proof-writing easier.</div><div><br></div><div>[type-natural]: https://hackage.haskell.org/package/type-natural</div><div>[equational-reasoning]: https://hackage.haskell.org/package/equational-reasoning</div><br><div>
-- Hiromi ISHII<br>konn.jinro@gmail.com<br><br><br>
</div>
<div><br><blockquote type="cite"><div>2023/01/13 19:02、Henning Thielemann <lemming@henning-thielemann.de>のメール:</div><br class="Apple-interchange-newline"><div><div><br>On Fri, 13 Jan 2023, rowan goemans wrote:<br><br><blockquote type="cite">I'm a heavy user of ghc-typelits-natnormalise.<br><br>I can feel your pain that it sometimes isn't able to solve seemingly "simple" constraints. But not all is lost in those cases. The `constraints` package allows one to solve `Nat` constraints out of thin air, provided you go through a function to do it.<br><br>nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0)<br>nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))<br></blockquote><br>Good to know that there are ways to add missing transformations.<br><br>Ideally there would be a way without unsafeCoerce, i.e. that I could prove a property manually using some proof steps expressed in functions.<br><br><br>Alternatively, maybe I can write missing steps in a custom type checker plugin.<br><br><br>Has someone already tried to connect SBV to a type checker plugin?<br>_______________________________________________<br>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe<br>Only members subscribed via the mailman list are allowed to post.</div></div></blockquote></div><br></body></html>