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


            
            kernelMVarBug.lean:5:15-5:20: error: failed to synthesize

            
              HAdd α α α

            
            Additional diagnostic information may be available using the `set_option diagnostics true` command.
	kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
	HAdd α α α
	Additional diagnostic information may be available using the `set_option diagnostics true` command.