Quelle  UnivBinders.out   Sprache: unbekannt

Inductive Empty@{uu} : Type@{uu} :=  .
(* uu |=  *)
Record PWrap@{uu} (A : Type@{uu}) : Type@{uu} := pwrap
  { punwrap : A }.
(* uu |=  *)

PWrap has primitive projections with eta conversion.
Arguments PWrap A%_type_scope
Arguments pwrap A%_type_scope punwrap
Arguments punwrap A%_type_scope p
Record PWrap@{uu} (A : Type@{uu}) : Type@{uu} := pwrap
  { punwrap : A }.
(* uu |=  *)

PWrap has primitive projections with eta conversion.
Arguments PWrap A%_type_scope
Arguments pwrap A%_type_scope punwrap
Arguments punwrap A%_type_scope p
Record RWrap@{uu} (A : Type@{uu}) : Type@{uu} := rwrap
  { runwrap : A }.
(* uu |=  *)

Arguments RWrap A%_type_scope
Arguments rwrap A%_type_scope runwrap
Arguments runwrap A%_type_scope r
runwrap@{uu} =
fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap
     : forall A : Type@{uu}, RWrap@{uu} A -> A
(* uu |=  *)

runwrap is a projection of RWrap
Arguments runwrap A%_type_scope r
Wrap@{uu} = fun A : Type@{uu} => A
     : Type@{uu} -> Type@{uu}
(* uu |=  *)

Arguments Wrap A%_type_scope
wrap@{uu} =
fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap
     : forall {A : Type@{uu}}, Wrap@{uu} A -> A
(* uu |=  *)

Arguments wrap {A}%_type_scope {Wrap}
bar@{uu} = nat
     : Wrap@{uu} Set
(* uu |= Set < uu *)
foo@{uu u v} =
Type@{u} -> Type@{v} -> Type@{uu}
     : Type@{max(uu+1,u+1,v+1)}
(* uu u v |=  *)
Type@{i} -> Type@{j}
     : Type@{max(i+1,j+1)}
(* {j i} |=  *)
     = Type@{i} -> Type@{j}
     : Type@{max(i+1,j+1)}
(* {j i} |=  *)
mono = Type@{mono.uu}
     : Type@{mono.uu+1}
mono
     : Type@{mono.uu+1}
Type@{mono.uu}
     : Type@{mono.uu+1}
File "./output/UnivBinders.v", line 50, characters 2-31:
The command has indeed failed with message:
Universe uu already exists.
monomono
     : Type@{MONOU+1}
mono.monomono
     : Type@{mono.MONOU+1}
monomono
     : Type@{MONOU+1}
mono
     : Type@{mono.uu+1}
File "./output/UnivBinders.v", line 70, characters 0-52:
The command has indeed failed with message:
Universe uu already exists.
bobmorane =
let tt := Type@{fooS.u1} in let ff := Type@{fooS.u3} in tt -> ff
     : Type@{max(fooS.u0,fooS.u2)}
File "./output/UnivBinders.v", line 87, characters 23-25:
The command has indeed failed with message:
Universe uu already bound.
foo@{E M N} =
Type@{M} -> Type@{N} -> Type@{E}
     : Type@{max(E+1,M+1,N+1)}
(* E M N |=  *)
foo@{uu u v} =
Type@{u} -> Type@{v} -> Type@{uu}
     : Type@{max(uu+1,u+1,v+1)}
(* uu u v |=  *)
foo@{u u IMPORTANT} =
Type@{u} -> Type@{IMPORTANT} -> Type@{u}
     : Type@{max(u+1,u+1,IMPORTANT+1)}
(* u u IMPORTANT |=  *)
Inductive Empty@{E} : Type@{E} :=  .
(* E |=  *)
Record PWrap@{E} (A : Type@{E}) : Type@{E} := pwrap
  { punwrap : A }.
(* E |=  *)

PWrap has primitive projections with eta conversion.
Arguments PWrap A%_type_scope
Arguments pwrap A%_type_scope punwrap
Arguments punwrap A%_type_scope p
punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
(* K |=  *)

punwrap is universe polymorphic
punwrap is a primitive projection of PWrap
Arguments punwrap A%_type_scope p
punwrap is transparent
Expands to: Constant UnivBinders.punwrap
Declared in library UnivBinders, line 12, characters 43-50
File "./output/UnivBinders.v", line 104, characters 0-19:
The command has indeed failed with message:
Universe instance length for foo is 3 but should be 1.
File "./output/UnivBinders.v", line 105, characters 0-20:
The command has indeed failed with message:
Universe instance length for mono is 0 but should be 1.
File "./output/UnivBinders.v", line 108, characters 0-33:
The command has indeed failed with message:
This object does not support universe names.
File "./output/UnivBinders.v", line 112, characters 0-50:
The command has indeed failed with message:
Cannot enforce v < u because u < gU < gV < v
insec@{v} = Type@{uu} -> Type@{v}
     : Type@{max(uu+1,v+1)}
(* v |=  *)
Inductive insecind@{k} : Type@{k+1} :=
    inseccstr : Type@{k} -> insecind@{k}.
(* k |=  *)

Arguments inseccstr _%_type_scope
insec@{uu v} = Type@{uu} -> Type@{v}
     : Type@{max(uu+1,v+1)}
(* uu v |=  *)
Inductive insecind@{uu k} : Type@{k+1} :=
    inseccstr : Type@{k} -> insecind@{uu k}.
(* uu k |=  *)

Arguments inseccstr _%_type_scope
insec2@{u} = Prop
     : Type@{Set+1}
(* u |=  *)
inmod@{uu} = Type@{uu}
     : Type@{uu+1}
(* uu |=  *)
SomeMod.inmod@{uu} = Type@{uu}
     : Type@{uu+1}
(* uu |=  *)
inmod@{uu} = Type@{uu}
     : Type@{uu+1}
(* uu |=  *)
Applied.infunct@{uu v} =
inmod@{uu} -> Type@{v}
     : Type@{max(uu+1,v+1)}
(* uu v |=  *)
axfoo@{i u u0} : Type@{u} -> Type@{i}
(* i u u0 |=  *)

axfoo is universe polymorphic
Arguments axfoo _%_type_scope
Expands to: Constant UnivBinders.axfoo
Declared in library UnivBinders, line 151, characters 6-11
axbar@{i u u0} : Type@{u0} -> Type@{i}
(* i u u0 |=  *)

axbar is universe polymorphic
Arguments axbar _%_type_scope
Expands to: Constant UnivBinders.axbar
Declared in library UnivBinders, line 151, characters 17-22
axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}

axfoo' is not universe polymorphic
Arguments axfoo' _%_type_scope
Expands to: Constant UnivBinders.axfoo'
Declared in library UnivBinders, line 152, characters 18-24
axbar' : Type@{axfoo'.u1} -> Type@{axfoo'.i}

axbar' is not universe polymorphic
Arguments axbar' _%_type_scope
Expands to: Constant UnivBinders.axbar'
Declared in library UnivBinders, line 152, characters 30-36
*** [ axfoo@{i u u0} : Type@{u} -> Type@{i} ]
(* i u u0 |=  *)

Arguments axfoo _%_type_scope
*** [ axbar@{i u u0} : Type@{u0} -> Type@{i} ]
(* i u u0 |=  *)

Arguments axbar _%_type_scope
*** [ axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} ]

Arguments axfoo' _%_type_scope
*** [ axbar' : Type@{axfoo'.u1} -> Type@{axfoo'.i} ]

Arguments axbar' _%_type_scope
File "./output/UnivBinders.v", line 158, characters 19-26:
The command has indeed failed with message:
When declaring multiple assumptions in one command, only the first name is
allowed to mention a universe binder (which will be shared by the whole
block).
foo@{i} = Type@{M.i} -> Type@{i}
     : Type@{max(M.i+1,i+1)}
(* i |=  *)
Type@{u0} -> Type@{UnivBinders.85}
     : Type@{max(u0+1,UnivBinders.85+1)}
(* {UnivBinders.85} |=  *)
bind_univs.mono = Type@{bind_univs.mono.u}
     : Type@{bind_univs.mono.u+1}
bind_univs.poly@{u} = Type@{u}
     : Type@{u+1}
(* u |=  *)
Inductive MutualR1@{u} (A : Type@{u}) : Prop :=
    Build_MutualR1 : MutualR2@{u} A -> MutualR1@{u} A
  with MutualR2@{u} (A : Type@{u}) : Prop :=
    Build_MutualR2 : MutualR1@{u} A -> MutualR2@{u} A.
(* u |=  *)

Arguments MutualR1 A%_type_scope
Arguments Build_MutualR1 A%_type_scope p1
Arguments p1 A%_type_scope m
Arguments MutualR2 A%_type_scope
Arguments Build_MutualR2 A%_type_scope p2
Arguments p2 A%_type_scope m
Inductive MutualI1@{u u0} (A : Type@{u}) : Type@{u0} :=
    C1 : MutualI2@{u u0} A -> MutualI1@{u u0} A
  with MutualI2@{u u0} (A : Type@{u}) : Type@{u0} :=
    C2 : MutualI1@{u u0} A -> MutualI2@{u u0} A.
(* u u0 |=  *)

Arguments MutualI1 A%_type_scope
Arguments C1 A%_type_scope p1
Arguments MutualI2 A%_type_scope
Arguments C2 A%_type_scope p2
CoInductive MutualR1'@{u} (A : Type@{u}) : Prop :=
    Build_MutualR1' : MutualR2'@{u} A -> MutualR1'@{u} A
  with MutualR2'@{u} (A : Type@{u}) : Prop :=
    Build_MutualR2' : MutualR1'@{u} A -> MutualR2'@{u} A.
(* u |=  *)

Arguments MutualR1' A%_type_scope
Arguments Build_MutualR1' A%_type_scope p1'
Arguments p1' A%_type_scope m
Arguments MutualR2' A%_type_scope
Arguments Build_MutualR2' A%_type_scope p2'
Arguments p2' A%_type_scope m
CoInductive MutualI1'@{u u0} (A : Type@{u}) : Type@{u0} :=
    C1' : MutualI2'@{u u0} A -> MutualI1'@{u u0} A
  with MutualI2'@{u u0} (A : Type@{u}) : Type@{u0} :=
    C2' : MutualI1'@{u u0} A -> MutualI2'@{u u0} A.
(* u u0 |=  *)

Arguments MutualI1' A%_type_scope
Arguments C1' A%_type_scope p1
Arguments MutualI2' A%_type_scope
Arguments C2' A%_type_scope p2
File "./output/UnivBinders.v", line 209, characters 0-33:
The command has indeed failed with message:
Universe inconsistency. Cannot enforce a < a because a = a.
JMeq :
forall [A : Type@{JMeq.u0}], A -> forall [B : Type@{JMeq.u1}], B -> Prop

JMeq is template universe polymorphic on JMeq.u0 (cannot be instantiated to Prop)
Arguments JMeq [A]%_type_scope x [B]%_type_scope _
Expands to: Inductive UnivBinders.PartialTemplate.JMeq
Declared in library UnivBinders, line 219, characters 10-14
File "./output/UnivBinders.v", line 234, characters 2-38:
The command has indeed failed with message:
Universe u0 already exists.
File "./output/UnivBinders.v", line 241, characters 6-26:
The command has indeed failed with message:
Tactic failure: Not equal (due to universes).
eq_rect
     : forall (A : Type@{eq_rect.u1}) (x : A) (P : A -> Type@{eq_rect.u0}),
       P x -> forall y : A, x = y -> P y
File "./output/UnivBinders.v", line 259, characters 18-19:
Warning: Separating sorts from universes with "|" is deprecated.
Use ";" instead.
[deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default]
File "./output/UnivBinders.v", line 259, characters 33-34:
Warning: Separating sorts from universes with "|" is deprecated.
Use ";" instead.
[deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default]
File "./output/UnivBinders.v", line 265, characters 16-17:
Warning: Separating sorts from universes with "|" is deprecated.
Use ";" instead.
[deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default]
id@{Prop ; Set}
     : forall A : Prop, A -> A
id@{SProp ; Set}
     : forall A : SProp, A -> A
id3@{s ; u} =
fun (A : Type@{s ; u}) (a : A) => a
     : forall A : Type@{s ; u}, A -> A
(* s ; u |= Set < u *)

Arguments id3 A%_type_scope a