bar : foo -> nat
bar is not universe polymorphic
bar is a projection of foo
Arguments bar id
bar is transparent
Expands to: Constant InductiveMainName.bar
Declared in library InductiveMainName, line 1, characters 16-19
bar' : foo' -> nat
bar' is not universe polymorphic
bar' is a projection of foo'
Arguments bar' {id'}
bar' is transparent
Expands to: Constant InductiveMainName.bar'
Declared in library InductiveMainName, line 3, characters 16-20
bar'' : foo'' -> foo''
bar'' is not universe polymorphic
bar'' is a projection of foo''
Arguments bar'' id''
bar'' is transparent
Expands to: Constant InductiveMainName.bar''
Declared in library InductiveMainName, line 5, characters 23-28
Record foo''' : Set := Build_foo''' { bar''' : nat } as id.
foo''' has primitive projections with eta conversion.
Arguments Build_foo''' bar'''%_nat_scope
Arguments bar''' id
[ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
]
