Commit 2023-06-25 08:53 b688e1a7

View on Github →

feat: port Archive.MiuLanguage.Basic (#5214)

Estimated changes

Modified Archive.lean

Created Archive/MiuLanguage/Basic.lean

added inductive Miu.Derivable

added def Miu.MiuAtom.repr

added inductive Miu.MiuAtom

added def Miu.Miustr.mrepr

added def Miu.Miustr

added def Miu.lcharToMiustr