| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
|
|
|
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
|
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
More dependencies / linking fixes.
|
