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


            
            example (n? : Option Nat) : False := by

            
              match h:n?, h':n? with

            
              | some 0, _ => {}
	example (n? : Option Nat) : False := by
	match h:n?, h':n? with
	\| some 0, _ => {}