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.

Link zu der Vergleichsansicht

pruefungen:hauptstudium:ls8:semprog_ss16 [07.10.2016 10:51] – angelegt koomipruefungen: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:
 +
 +<code>
 +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).
 +</code>
 +
 +