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


            
            example (x : Nat) : True :=

            
            match h:x with


            section end


            structure A where

            
            h : Nat := 1

            
            h2 : h ≠ 0 := by
	example (x : Nat) : True :=
	match h:x with

	section end

	structure A where
	h : Nat := 1
	h2 : h ≠ 0 := by