How to fix "unknown package 'data'" for Lean 4

Stream: lean4

[Henrik Böving]

If you are using a package called data you are either using code from or following a tutorial for Lean 3 and not Lean 4 so the fix is one of: switch to lean 3 or use Lean 4 code/tutorials