search

JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Create FiniteMultiset.ard #56

Open ice1000 opened 1 year ago

ice1000 commented 1 year ago

This is an interesting demonstration of higher inductive types.