Zulip Chat Archive

Stream: general

Topic: universe issues


view this post on Zulip Eric Wieser (Feb 10 2021 at 09:46):

Why does this work with a general ι, but fail with fin 2?

import data.fin

/-- A value which wraps a type. -/
inductive typeinfo (α : Type*) : Type
| of [] : typeinfo

/-- Get the type of the domain of a function type. -/
abbreviation {u} typeinfo.domain {α : Type u} {β : α  Type*}
  (a : typeinfo (Π (i : α), β i)) : Type u := α

/-- Get the type of the codomain of a function type. -/
abbreviation {u} typeinfo.codomain {α : Type*} {β : Type u}
  (a : typeinfo (α  β)) : Type u := β

/-- Get the type of the codomain of a dependent function type. -/
abbreviation {u} typeinfo.pi_codomain {α : Type*} {β : α  Type u}
  (a : typeinfo (Π (i : α), β i)) : α  Type u := β

variables {M' : Type*}  {ι : Type*}

#check (ι  M')
#check typeinfo (ι  M')
#check typeinfo.of (ι  M')
#check typeinfo.domain (typeinfo.of (ι  M'))

#check (fin 2  M')
#check typeinfo (fin 2  M')
#check typeinfo.of (fin 2  M')
#check typeinfo.domain (typeinfo.of (fin 2  M'))  -- fail, everything else works

view this post on Zulip Chris Hughes (Feb 10 2021 at 10:34):

The : _ trick works #check typeinfo.domain (typeinfo.of (fin 2 → M') : _). Not sure if that's helpful really though.

view this post on Zulip Eric Wieser (Feb 10 2021 at 10:39):

Unfortunately adding : _ in my larger context of using this for notation in #6152 makes it ineligible for pretty-printing

view this post on Zulip Eric Wieser (Feb 10 2021 at 10:56):

But it does fix the problem

view this post on Zulip Eric Wieser (Feb 10 2021 at 10:58):

attribute [elab_simple] typeinfo.of fixes it!


Last updated: May 12 2021 at 23:13 UTC