tests/lean/2125.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            open Classical


            noncomputable def f (α : Type) : Bool :=

            
              Nonempty α


            -- The following inductive is unsound:

            
            inductive C : Bool → Type

            
              -- Must be rejected because `C` occurs inside an index.

            
              | c : C (f (C false))
	open Classical

	noncomputable def f (α : Type) : Bool :=
	Nonempty α

	-- The following inductive is unsound:
	inductive C : Bool → Type
	-- Must be rejected because `C` occurs inside an index.
	\| c : C (f (C false))