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


            
            /-! should not parse `done` as part of `induction` -/


            example (a : Nat) : True := by

            
              induction a with

            
              done
	/-! should not parse `done` as part of `induction` -/

	example (a : Nat) : True := by
	induction a with
	done