Ich hoffe, die Änderungen kommen noch nicht zu spät. Die restliche Story werde ich jetzt erstmal nicht anfassen.
Die Syntax für Lean-Code in Hints verstehe ich nicht, und sie scheint mir auch nicht einheitlich. Was ist der Unterschied zwischen A und {A}? Ist es OK, unicode für → etc. zu verwenden?
In Contradiction/L01 steht ". Hint" statt "Hint" am Anfang der Zeile. Ist das richtig?
Wir hatten mal darüber geredet, https://en.wikipedia.org/wiki/Drinker_paradox einzubauen. Ist das schon irgendwo, oder ist das zu kompliziert? Man braucht, um das zu formulieren, Prädikate, die von Variablen abhängen.
Ich hoffe, die Änderungen kommen noch nicht zu spät. Die restliche Story werde ich jetzt erstmal nicht anfassen.
Die Syntax für Lean-Code in Hints verstehe ich nicht, und sie scheint mir auch nicht einheitlich. Was ist der Unterschied zwischen
Aund{A}? Ist es OK, unicode für → etc. zu verwenden?In Contradiction/L01 steht ". Hint" statt "Hint" am Anfang der Zeile. Ist das richtig?
Wir hatten mal darüber geredet, https://en.wikipedia.org/wiki/Drinker_paradox einzubauen. Ist das schon irgendwo, oder ist das zu kompliziert? Man braucht, um das zu formulieren, Prädikate, die von Variablen abhängen.