Skip to content

Impredicative set broken with inductives #21233

New issue
New issue
Open
Open
Impredicative set broken with inductives#21233
Labels
kind: bugAn error, flaw, fault or unintended behaviour.part: inductivesInductive types, fixpoints, etc.part: universesThe universe system.
@SkySkimmer

Description

@SkySkimmer
SkySkimmer
opened on Oct 27, 2025
(* coq-prog-args: ("-impredicative-set") *)
Inductive X : Set := x (_:Set).
(* Error: Universe inconsistency. Cannot enforce Set+1 <= Set. *)

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugAn error, flaw, fault or unintended behaviour.part: inductivesInductive types, fixpoints, etc.part: universesThe universe system.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions