combined check and simp command

Stream: lean4

[Chris Henson]

Is there a command similiar to #check that also simplifies the type, possibly with simp?

[Damiano Testa]

Is #simp ... a thing?

[Damiano Testa]

docs#Mathlib.Tactic.Conv.«command#simpOnly_=>__», maybe?

[Yaël Dillies]

Yes, but it only simplifies the expression. It does not infer the type. #simp %type_of your_thing should do

[Damiano Testa]

Ah, I had missed "simplifying the type"!

[Floris van Doorn]

Yael's code has a small typo. This works:

import Mathlib.Tactic

#simp type_of% true

[Yaël Dillies]

Argh, I was trying really hard to remember which side the % went on :see_no_evil:

[Chris Henson]

No worries, I figured it out. Thanks!

[Damiano Testa]

It should go where a percentage would go, right?

[Damiano Testa]

This is also how I remember # and % in bash...

[Yaël Dillies]

Damiano Testa said:

It should go where a percentage would go, right?

Well actually I thought it went at the start because no Lean identifier can start with it

[Damiano Testa]

I see, but that mnemonic gives the wrong answer... :smile:

[Yaël Dillies]

Do you have a mnemonic for which mnemonic gives the right answer? :dizzy:

[Damiano Testa]

:lol: I had not thought of yours, so I simply went for where I would expect the symbol to go:

• my first reaction to # is a cardinality and I place it before the object,
• my first reaction to % is a percentage and I place it after the object.

[Kyle Miller]

With # I think "time to start a command" and with % I think "oh right, this was a special elaborator"