Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » semprog_ss16 (Übersicht)
Unterschiede
Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.
pruefungen:hauptstudium:ls8:semprog_ss16 [07.10.2016 10:51] – angelegt koomi | pruefungen:hauptstudium:ls8:semprog_ss16 [03.08.2019 09:02] (aktuell) – Marcel[Inf] | ||
---|---|---|---|
Zeile 62: | Zeile 62: | ||
We stopped after I backwards-reasoned one instance of the assignment rule (which took several attempts). | We stopped after I backwards-reasoned one instance of the assignment rule (which took several attempts). | ||
+ | |||
+ | |||
+ | ---- | ||
+ | |||
+ | The text below has been written by a student from the future different from the author of the exam protocol above! | ||
+ | |||
+ | Here is some working Coq code for the no_repeats inductive question: | ||
+ | |||
+ | < | ||
+ | Fixpoint appears_not_in {X: Type} (x: X) (l: list X): Prop := match l with | ||
+ | | nil => True | ||
+ | | cons y ys => (x <> y) /\ (appears_not_in x ys) | ||
+ | end. | ||
+ | |||
+ | Inductive no_repeats {X: Type} : list X -> Prop := | ||
+ | | nor_empty: no_repeats nil | ||
+ | | nor_cons: forall x l, appears_not_in x l -> no_repeats l -> no_repeats (x::l). | ||
+ | </ | ||
+ | |||
+ |