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


            
            inductive Foo {x : Nat} : Type where

            
              | foo : Foo


            def bar := (fun _ : Foo => 0) Foo.foo
	inductive Foo {x : Nat} : Type where
	\| foo : Foo

	def bar := (fun _ : Foo => 0) Foo.foo