search

JamesGallicchio / LeanColls

WIP collections library for Lean 4
https://jamesgallicchio.github.io/LeanColls/docs/
Apache License 2.0
30 stars 7 forks source link

`Index.card` has an extra universe parameter #27

Open JamesGallicchio opened 5 months ago

JamesGallicchio commented 5 months ago

As in title.

set_option pp.universes true
#check IndexType.card (Prod (Fin 2) (Fin 2))
-- IndexType.card.{0, u_1} (Prod.{0, 0} (Fin 2) (Fin 2))

Probably we should not require Fold in the definition of IndexType, instead just expecting the universe to be Fold at any functions that need it.