Zulip Chat Archive

Stream: lean4

Topic: polytype lists

Arthur Paulino (Nov 24 2021 at 21:53):

In my current code I'm needing to do
mysql.insertIntoTable "cars" ["1", "'audi'", "50000"]
But I'd like to be able to say
mysql.insertIntoTable "cars" [1, "audi", 50000]
Any idea how to achieve it or something similarly easy to use?

Last updated: Dec 20 2023 at 11:08 UTC