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


            
            def foo: Unit := ()

            
            where

            
              bar: (_: Unit) → {n : Nat} → Fin n → Fin n

            
              | _, _, _ => sorry


            #check foo.bar
	def foo: Unit := ()
	where
	bar: (_: Unit) → {n : Nat} → Fin n → Fin n
	\| _, _, _ => sorry

	#check foo.bar