This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* The following two examples fulfill the (strict) positivity condition *) | |
Inductive Switch (A : Type) : Type := | |
| switch : Switch A -> Switch A. | |
Inductive UseSwitch := | |
| useSwitch : Switch UseSwitch -> UseSwitch. | |
Inductive SwitchSP (A : Type) : Type := |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-------------------------------- | |
-- Pretty Printing type class -- | |
-------------------------------- | |
class Pretty a where | |
pretty :: a -> String | |
pprint :: a -> IO () | |
pprint = putStrLn . pretty | |
instance Pretty Int where |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Lists.List. | |
Require Import Arith.Arith. | |
Require Import Omega. | |
Set Implicit Arguments. | |
Fixpoint replicate A (n : nat) (x : A) : list A := | |
match n with | |
| O => nil |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Set Implicit Arguments. | |
Inductive Simple (A: Type) := simple : Simple A. | |
Inductive Wrap (A: Type) := | |
| wrap : A -> Wrap A | |
| funWrap : forall X, Simple X -> (X -> Wrap A) -> Wrap A. | |
Definition anotherWrap A : Wrap A := | |
funWrap (simple A) (fun x => wrap x). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Coq.Arith.PeanoNat. | |
Definition VarIndex := nat. | |
Parameter atom : Set. | |
Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}. | |
Section expr_ind. | |
Inductive Expr : Type := | |
| BVar : VarIndex -> VarIndex -> Expr |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# min_sort | |
def min_sort(to_sort) | |
length = to_sort.length - 1 | |
min_index = nil | |
for i in 0..length | |
min_index = i | |
for j in i..length | |
if to_sort[j] < to_sort[min_index] | |
min_index = j |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Language: Ruby, Level: Level 1 | |
# Präsenzaufgabe - Programmsimulation | |
n = 10; #1 | |
sum = 0; #2 | |
zaehler = 1; #3 | |
while zaehler <= n do | |
sum = sum + zaehler; #4 | |
zaehler = zaehler + 1; #5 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Language: Ruby, Level: Level 1 | |
# Präsenzaufgabe 1 - Programmsimulation | |
n = 10; #1 | |
sum = 0; #2 | |
zaehler = 1; #3 | |
while zaehler <= n do | |
sum = sum + zaehler; #4 | |
zaehler = zaehler + 1; #5 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Language: Ruby, Level: Level 1 | |
## | |
## Übungsbetrieb vom 4.11.2015 | |
## | |
## alle mit `#` beginnenden Zeilen sind Kommentare | |
## | |
## Präsenzaufgabe 1 | |
x = true; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Language: Ruby, Level: Level 1 | |
## | |
## Übungsbetrieb vom 5.11.2015 | |
## | |
## alle mit `#` beginnenden Zeilen sind Kommentare | |
## | |
## Präsenzaufgabe 1 |
NewerOlder