Zulip Chat Archive

Stream: new members

Topic: simp


view this post on Zulip petercommand (Nov 15 2018 at 04:56):

is it possible to tell which rules/lemmas simp used to simplify a type?

view this post on Zulip Mario Carneiro (Nov 15 2018 at 04:58):

use squeeze_simp

view this post on Zulip Mario Carneiro (Nov 15 2018 at 04:58):

or set_option trace.simplify.rewrite true

view this post on Zulip petercommand (Nov 15 2018 at 04:59):

thanks!

view this post on Zulip petercommand (Nov 15 2018 at 05:00):

will try both

view this post on Zulip toc (Sep 03 2020 at 16:38):

If I've got

 k * (a * k_n) + k * (b * k_m) = a * (k * k_n) + b * (k * k_m)

this _seems_ like something I should be able to just simp. Am I missing imports or something similar?

view this post on Zulip Ruben Van de Velde (Sep 03 2020 at 16:40):

I'd be somewhat surprised if simp worked on that, but maybe ring will?

view this post on Zulip toc (Sep 03 2020 at 16:46):

Well that got me

type mismatch at application
  tactic.istep 102 0 102 0 ring
term
  ring
has type
  Type ?  Type ? : Type (?+1)
but is expected to have type
  tactic ?m_1 : Type ?

is ring supposed to be the "do some algebra" tactic, then?

view this post on Zulip Bryan Gin-ge Chen (Sep 03 2020 at 16:46):

That looks like you haven't put import tactic at the top of your file.

view this post on Zulip Bryan Gin-ge Chen (Sep 03 2020 at 16:47):

Here's the documentation on ring: tactic#ring

view this post on Zulip toc (Sep 03 2020 at 16:51):

(trying that now, it is... taking a while to load/run)

view this post on Zulip toc (Sep 03 2020 at 16:52):

But that did ultimately work. Thanks!

view this post on Zulip Bryan Gin-ge Chen (Sep 03 2020 at 16:55):

I think you'll hit the limits of the web editor pretty soon. I'd definitely recommend following the directions here #install if at all possible.

view this post on Zulip toc (Sep 03 2020 at 17:07):

Yep! I'm in vscode now.


Last updated: May 12 2021 at 04:19 UTC