tests/lean/277b.lean.expected.out - third_party/github.com/leanprover/lean4 - Git at Google


            
            277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor

            
              List Point
	277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor
	List Point