Why/when can I not replace a type by a def synonm?

Stream: new members

[Malvin Gattinger]

inductive Step : Nat → Type
| base : Step 0
| whatever : Step k

def SomeStep := Σ n, Step n

def History := List SomeStep -- Does this make them synonyms?

inductive StepList : List SomeStep → Type -- When I replace "List SomeStep'" with "History" ...
| nil : StepList []
| step : (s : Step m) → StepList L → StepList (⟨_,s⟩ :: L)
| rep : (⟨_,s⟩ : SomeStep) ∈ L → StepList L
-- ... then the "rep" case triggers errors missing the instance
--   Membership ((n : Nat) × Step n) History
-- even though I cast it to be a SomeStep.

The same happens with using a one field structure instead of the def above:

 structure History := h : List SomeStep

[Kevin Buzzard]

def History := List SomeStep makes them defeq, but typeclass inference won't unfold the definition. Use abbrev if you want typeclass inference to see through it.

import Mathlib.Tactic

def foo := ℕ
abbrev bar := ℕ

example : foo := 37 -- fails
example : bar := 37 -- succeeds

(numerals are powered by typeclass inference, like \in is).

[Malvin Gattinger]

Ah, I did not know abbrev yet. Perfect, thank you!

[Kevin Buzzard]

abbrev is close to (or possibly even equal to) @[inline, reducible].