Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Wie verwendet man flatseq (bzw sequences)
Ist mehr eine Verständnisfrage. Wie verwendet man flatseq ? Wenn ich zum Beispiel folgendes schreibe :
A : NAT |
bla : NAT ^ (succ one) | = ⟨ A , A⟩ |
Bekomme ich einen Fehler , dass der Typ nicht richtig inferiert werden kann.
Des weiteren bekomme ich es leider nicht hin die natlits aus dem Foundation von MitM damit zu verwenden.
So bald ich die Include und so was hier mache :
include base:?NatLiterals ❙
include seq:?LFS ❙
bla : ℕ ^ ((1) : ℕ) ❙
bekomme ich eben den Fehler , dass “1” kein NAT ist (dachte nur , dass das möglich ist, an dieser Stelle ℕ zu verwenden , da ℕ ja irgendwie über NAT definiert sein soll , auch wenn ich das nicht in math.mmt sehe … )
Am besten im moment gar nicht.
Ja, das rechts ist auch keine Sequenz (im Sinne von flatseq). Das ganze ist etwas komplizierter (Die Intention von flatseq ist es, „sequenzen-argumente“ für flexäre operatoren zuzulassen - sequenzen sind also kein „echter typ“ von „Folgen“ oder sowas); ich empfehle tatsächlich das ganze einfach nicht zu benutzen. Unter anderem weil Literals da wie du sagst schwierigkeiten verursachen können.