Zulip Chat Archive

Stream: Is there code for X?

Topic: Reading a file

Ami Ashman (Mar 13 2023 at 15:02):

Hi! I'm just starting to learn Lean and writing a program that takes data in the form of CSV. Is there a way to read directly from a CSV file? I've just been copy-pasting into lean so far. Thanks!

Alex J. Best (Mar 13 2023 at 15:06):

Lean 3 or lean 4?

Ami Ashman (Mar 13 2023 at 15:24):

I'm using Lean 4

Alex J. Best (Mar 13 2023 at 15:28):

Ok, then I recommend this blog post: https://agentultra.github.io/lean-4-hackers/ and you can parse csv on top of that fairly easily

Alex J. Best (Mar 13 2023 at 15:29):

You can go more complicated if needed, e.g https://github.com/leanprover/lean4-samples/tree/main/CSVParser but for simple examples just splitting on commas works fine

Last updated: Dec 20 2023 at 11:08 UTC