slate hlm

Der Slate Interactive Theorem Prover

Slate ist ein interaktiver Theorem -Prover, der derzeit in der Entwicklung befindet. Dieses Repository enthält seine Standardbibliothek.

Webzugriff

Slate ist als Webanwendung konzipiert. Die gesamte Bibliothek kann über die Webschnittstelle unter https://slateprover.org/ bearbeitet werden.

Die Weboberfläche erstellt automatisch persönliche Gabeln dieses Repositorys für jeden Mitwirkenden und sendet Einsendungen als Pull -Anfragen.

Lokale Entwicklung

Für komplexere Aufgaben empfehlen wir die Erweiterung für Microsoft Visual Studio Code. Bitte befolgen Sie die Anweisungen auf dieser Seite.

Das Slate -Repository enthält die Bibliothek als Git -Submodul. Um lokale Änderungen hochzuladen, müssen Sie Ihre eigene Gabel als Git -Fernbedienung für dieses Submodul hinzufügen.