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


            
            inductive T

            
              | t : T


            @[reducible] def T.eval : T → Type

            
              | T.t => Int


            def T.default (τ : T) : τ.eval :=

            
              match τ, τ.eval with

            
              | T.t, .(Int) => (0 : Int)
	inductive T
	\| t : T

	@[reducible] def T.eval : T → Type
	\| T.t => Int

	def T.default (τ : T) : τ.eval :=
	match τ, τ.eval with
	\| T.t, .(Int) => (0 : Int)