aya-prover/aya-dev

Once we're up to lowercase package names, `data` conflict with the keyword

ice1000 opened this issue · 1 comments

ice1000 commented

I think we should rename to inductive

ice1000 commented

Now it's obvious why Lean chose inductive!

  • 😄1