`simp?`

tactic #

The `simp?`

tactic is a simple wrapper around the simp with trace behavior implemented in core.

The common arguments of `simp?`

and `simp?!`

.

## Equations

- One or more equations did not get rendered due to their size.

`simp?`

takes the same arguments as `simp`

, but reports an equivalent call to `simp only`

that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.

```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all`

and `dsimp`

.

## Equations

- One or more equations did not get rendered due to their size.

`simp?`

takes the same arguments as `simp`

, but reports an equivalent call to `simp only`

that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.

```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all`

and `dsimp`

.

## Equations

- One or more equations did not get rendered due to their size.

The common arguments of `simp_all?`

and `simp_all?!`

.

## Equations

- One or more equations did not get rendered due to their size.

`simp?`

takes the same arguments as `simp`

, but reports an equivalent call to `simp only`

that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.

```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all`

and `dsimp`

.

## Equations

- One or more equations did not get rendered due to their size.

`simp?`

takes the same arguments as `simp`

, but reports an equivalent call to `simp only`

that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.

```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all`

and `dsimp`

.

## Equations

- One or more equations did not get rendered due to their size.

The common arguments of `dsimp?`

and `dsimp?!`

.

## Equations

- One or more equations did not get rendered due to their size.

`simp?`

takes the same arguments as `simp`

, but reports an equivalent call to `simp only`

that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.

```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all`

and `dsimp`

.

## Equations

- One or more equations did not get rendered due to their size.

`simp?`

takes the same arguments as `simp`

, but reports an equivalent call to `simp only`

that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.

```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all`

and `dsimp`

.

## Equations

- One or more equations did not get rendered due to their size.