osa1

{-# LANGUAGE LambdaCase #-}

fib :: Integer -> Integer
fib 0 = 1
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

fib' :: Integer -> Integer
fib' = \case
         0 -> 1

osa1

diff --git a/src/Compiler/Settings.hs b/src/Compiler/Settings.hs
index 55c3472..f340cee 100644
--- a/src/Compiler/Settings.hs
+++ b/src/Compiler/Settings.hs
@@ -50,3 +50,6 @@ newGhcjsEnv = GhcjsEnv <$> newMVar M.empty
 buildingDebug :: DynFlags -> Bool
 buildingDebug dflags = WayDebug `elem` ways dflags
 
+buildingProf :: DynFlags -> Bool
+buildingProf dflags = WayProf `elem` ways dflags

osa1

module Main where

import GHC.Stack

newtype M s a = M { unM :: s -> (s, a) }

instance Monad (M s) where
    (M m) >>= k = M $ \s -> case m s of
                              (s', a) -> unM (k a) s'
    return a = M $ \s -> (s, a)

osa1

Require Import List.
Import ListNotations.

Open Scope list_scope.

Inductive semigroup (A : Type) (Op : A -> A -> A) : Prop :=
| Semigroup_intro :
    (forall (a1 a2 a3 : A), Op a1 (Op a2 a3) = Op (Op a1 a2) a3) -> semigroup A Op.

osa1

Require Import List.
Import ListNotations.
Open Scope list_scope.
Require Import Arith.
Require Import Omega.
Require Import Permutation.

Inductive sorted : list nat -> Prop :=
| Sorted_nil : sorted []
| Sorted_singleton : forall e, sorted [e]

osa1

Require Import Omega.
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.VectorDef.
Open Scope vector_scope.
Require Import List.
Require Import Arith.

CoInductive triangle_t (T : Type) : nat -> Type :=
| triangle : forall (n : nat), Vector.t T n -> triangle_t T (S n) -> triangle_t T n.

osa1

import Prelude.Vect

%default total

sumPairs : Vect (S n) Nat -> Vect n Nat
sumPairs (h1 :: h2 :: tl) = (h1 + h2) :: sumPairs (h2 :: tl)
sumPairs [h]              = []

-- try to show how non-top-level pattern matching won't work

osa1

%default total

class Cardinality (a : Type) (n : Nat) where
  toFin         : a -> Fin n
  fromFin       : Fin n -> a
  bijective     : (a' : a) -> fromFin (toFin a') = a'
  bijective_inv : (f : Fin n) -> toFin (fromFin f) = f

data T = A | B | C

osa1

diff --git k-core/src/main/java/org/kframework/backend/java/symbolic/KILtoBackendJavaKILTransformer.java k-core/src/main/java/org/kframework/backend/java/symbolic/KILtoBackendJavaKILTransformer.java
index 12ab701..28f9aca 100644
--- k-core/src/main/java/org/kframework/backend/java/symbolic/KILtoBackendJavaKILTransformer.java
+++ k-core/src/main/java/org/kframework/backend/java/symbolic/KILtoBackendJavaKILTransformer.java
@@ -537,11 +537,11 @@ public class KILtoBackendJavaKILTransformer extends CopyOnWriteTransformer {
         java.util.Map<CellLabel, Term> lhsOfReadCell = null;
         java.util.Map<CellLabel, Term> rhsOfWriteCell = null;
         if (ruleData.isCompiledForFastRewriting()) {
-            lhsOfReadCell = Maps.newHashMap();
+            lhsOfReadCell = Maps.newLinkedHashMap();

osa1

module Cardinality where

open import Data.Bool using (Bool; true; false)
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function