simp

Stream: new members

[petercommand]

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

[Mario Carneiro]

use squeeze_simp

[Mario Carneiro]

or set_option trace.simplify.rewrite true

[petercommand]

thanks!

[petercommand]

will try both

[toc]

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?

[Ruben Van de Velde]

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

[toc]

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?

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

Here's the documentation on ring: tactic#ring

[toc]

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

[toc]

But that did ultimately work. Thanks!

[Bryan Gin-ge Chen]

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.

[toc]

Yep! I'm in vscode now.