levi civita field release

Stream: general

[Eric Wieser]

Alok Singh said:

https://github.com/alok/lean-inf

this is a computational implementation based on https://github.com/khafatech/inf. the core data type LeviCivitaNum is implemented, front end of calculator is WIP.

a good example of sorry friendly programming (Tomas Skrivan)

It looks like something is wrong with your repo, the inf folder is missing

[Notification Bot]

A message was moved here from #announce > levi civita field release by Eric Wieser.

[Eric Wieser]

Ah, I now see that the library is all in the :/Main.lean file not in :/LeanInf, which is why I couldn't find it!

[Alok Singh]

feel free to put in a pr, else i’ll organize the code sometime this week

[Eric Wieser]

This is the inf folder I mean:

image.png