Skip to content

Define [tele_arg] as a fixpoint

Gregory Malecha requested to merge gmalecha/stdpp:fixpoint-tele_arg into master

The current definition of tele_arg increases the universe level in a way that is unfortunate. In particular,

Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...

In Iris, what this means is that bi_tforall/bi_texist have different universe levels than bi_forall/bi_exist. This MR re-defines tele_arg as a fixpoint, which prevents the universe bump. In particular:

Fixpoint tele_arg (t : tele@{u}) : Type@{u} :=
  ...

With this definition, the universes for the telescopic quantifiers can match the universes of the non-telescopic quantifiers in iris (this enables a separate MR to iris: iris!781 (merged)).

Edited by Gregory Malecha

Merge request reports