why #reduce doesnt reduce abbrevs? I want to see type

Stream: new members

[Serhii Khoma (srghma)]

I have

abbrev arrow (α : ι → Type v) (β : ι → Type w) (i : ι) := α i → β i
abbrev product (α : ι → Type v) (β : ι → Type w) (i : ι) := α i × β i
abbrev bind (α : ι → Type v) := ∀{n}, α n
abbrev const (α : Type c) (_ : ι) := α

-- Regular arrow have precedence 25
infixr:29 " ⟶ " => arrow
infixr:35 " ⊗ " => product
prefix:38 "κ " => const
notation:27 "⟦ " α " ⟧" => bind α

abbrev Box (α : Nat → Type u) (n : Nat) : Type u := ∀{m}, m < n → α m
prefix:40 "□ " => Box

set_option pp.all true
set_option pp.notation false

def fixbx := fun α => ⟦ □ α ⟶ α ⟧ → ⟦ □ α ⟧

#print fixbx
-- PRINTS
-- def fixbx.{u_1} : (α : Nat → Type u_1) → Type u_1 :=
-- fun (α : Nat → Type u_1) ↦
--   @_root_.bind.{u_1, 1} Nat (@arrow.{u_1, u_1, 1} Nat (Box.{u_1} α) α) → @_root_.bind.{u_1, 1} Nat (Box.{u_1} α)

#check fixbx
-- PRINTS
-- fixbx.{u_1} (α : Nat → Type u_1) : Type u_1

#reduce fixbx
-- PRINTS
-- fun (α : Nat → Type u_1) ↦
-- @_root_.bind.{u_1, 1} Nat (@arrow.{u_1, u_1, 1} Nat (Box.{u_1} α) α) → @_root_.bind.{u_1, 1} Nat (Box.{u_1} α)

but I want too see unabbreviated. Something like

fun (α : Nat → Type u_1) ↦
  (∀ {n : Nat}, ∀ {m : Nat}, m < n → α m → α n) → ∀ {n : Nat}, ∀ {m : Nat}, m < n → α m

How to?

[Kyle Miller]

Maybe #reduce (types := true) fixbx?

[Serhii Khoma (srghma)]

tnx

#reduce (types := true) fixbx will print fun α ↦ _root_.bind (□ α ⟶ α) → {n m : Nat} → m < n → α m

---

set_option pp.all true
#reduce (types := true) fixbx

will print

fun (α : Nat → Type u_1) ↦
@_root_.bind.{u_1, 1} Nat (@arrow.{u_1, u_1, 1} Nat (Box.{u_1} α) α) →
  {n m : Nat} → @LT.lt.{0} Nat instLTNat m n → α m

---

set_option pp.all true
set_option pp.notation false
#reduce (types := true) fixbx

will print

fun (α : Nat → Type u_1) ↦
@_root_.bind.{u_1, 1} Nat (@arrow.{u_1, u_1, 1} Nat (Box.{u_1} α) α) →
  {n m : Nat} → @LT.lt.{0} Nat instLTNat m n → α m

---

First variant is the best

is there a way to also reduce argument _root_.bind (□ α ⟶ α) in fun α ↦ _root_.bind (□ α ⟶ α) → {n m : Nat} → m < n → α m?

Also tried (proofs := true) - same output

[Serhii Khoma (srghma)]

I have found hacky approach

example : ⟦ □ α ⟶ α ⟧ → ⟦ □ α ⟧ = (⟦ □ α ⟶ α ⟧ → ⟦ □ α ⟧) := by
  unfold _root_.bind Box arrow
  rfl

and thus I can unfold only e.g. Box or bind or arrow and what the function exactly is without them