lean

5Ciepło

1Odpowiedz

Jak definiować wzajemne propozycje indukcyjne w Lean?

Próbuję użyć składni indukcyjnych typów danych, ale otrzymałem komunikat o błędzie "typy wzajemnie indukcyjne muszą się kompilować z podstawowym typem indukcyjnym z zależną eliminacją". Poniżej jest p