diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-12 13:29:16 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-03 13:37:56 +0200 |
| commit | 4361c1ed9ac5646055f9f0eecc4a003d720c1994 (patch) | |
| tree | 773a5acaa5099e447eca5a62bd9d3e478a4a8e89 /interp | |
| parent | e9b745af47ba3386724b874e3fd74b6dad33b015 (diff) | |
Type@{_} should not produce a flexible algebraic universe.
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions