Auswahl Schwarzes Brett Aktion im Forum Suche Kontakt Für Mitglieder Mathematisch für Anfänger Wer ist Online | |
Autor |
Umstellung von ISO8859 auf UTF8 beendet |
|
tactac
Senior  Dabei seit: 15.10.2014 Mitteilungen: 1500
 |     Beitrag No.40, eingetragen 2018-10-11
|
2018-10-11 22:51 - matroid in Beitrag No. 39 schreibt:
2018-10-10 00:33 - tactac in Beitrag No. 37 schreibt:
Sehr schön. Nur schwach verwandtes Thema: An deinem Code-Beispiel fällt auf, dass dem Syntax-Highlighting für Lean die gehörige Bünte fehlt.  Aber wenigstens geht das schonmal:
Hi tactac,
bitte sende mir eine Datei mit dem Code per Mail.
Gruß
Matroid
Okay.
|
Profil
Quote
Link |
matroid
Senior  Dabei seit: 12.03.2001 Mitteilungen: 13888
Aus: Solingen
 |     Beitrag No.41, vom Themenstarter, eingetragen 2018-10-12
|
Profil
Quote
Link |
matroid
Senior  Dabei seit: 12.03.2001 Mitteilungen: 13888
Aus: Solingen
 |     Beitrag No.42, vom Themenstarter, eingetragen 2018-10-14
|
Danke für die Datei. Ich habe noch ein fehlendes Komma am Ende von Zeile 139 ergänzt. Dann sieht es nun so aus:
Lean constant c : ℕ
constants (d e : ℕ) (f : ℕ → ℕ)
axiom cd_eq : c = d
def foo : ℕ := 5
def bar := 6
def baz (x y : ℕ) (s : list ℕ) := [x, y] ++ s
theorem foo_eq_five : foo = 5 := rfl
theorem baz_theorem (x y : ℕ) : baz x y [] = [x, y] := rfl
lemma baz_lemma (x y : ℕ) : baz x y [] = [x, y] := rfl
example (x y : ℕ) : baz x y [] = [x, y] := rfl |
Gruß
Matroid
|
Profil
Quote
Link |
tactac
Senior  Dabei seit: 15.10.2014 Mitteilungen: 1500
 |     Beitrag No.43, eingetragen 2018-10-14
|
2018-10-14 19:30 - matroid in Beitrag No. 42 schreibt:
Danke für die Datei. Ich habe noch ein fehlendes Komma am Ende von Zeile 139 ergänzt. Dann sieht es nun so aus:
[...] Schön. :-)
|
Profil
Quote
Link |
|