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


            
            refineOccursCheck.lean:11:2-11:14: error: 'refine' tactic failed, value

            
              ax ?a

            
            depends on the main goal metavariable '?a'
	refineOccursCheck.lean:11:2-11:14: error: 'refine' tactic failed, value
	ax ?a
	depends on the main goal metavariable '?a'