This file contains 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
open import Data.Nat | |
open import Data.Fin hiding (_+_) | |
open import Data.Product | |
import Relation.Binary.HeterogeneousEquality as H | |
Types : Set₁ | |
Types = ℕ → Set | |
Seq : Types → Set | |
Seq t = (n : ℕ) → t n |
This file contains 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
------------------------------ MODULE Blinkers ------------------------------ | |
EXTENDS Integers | |
VARIABLES x , y | |
Init1 == x = 1 | |
Init2 == y = 1 |
This file contains 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
import Relation.Binary.PropositionalEquality as P | |
open import Data.List using (List ; [] ; _∷_ ; tabulate ; lookup ; filter) | |
open import Relation.Nullary | |
import Function as F | |
e : ∀{ℓ} → {A : Set ℓ} → (∀ (x y : A) → Dec (x P.≡ y)) → List A → List A |
This file contains 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
open import Data.Nat as ℕ | |
open import Data.Fin hiding (inject≤) | |
open import Relation.Binary.PropositionalEquality | |
inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n | |
inject≤ {_} {suc n} zero le = zero | |
inject≤ {_} {suc n} (suc i) le = suc (inject≤ i (ℕ.≤-pred le)) |
This file contains 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
open import Prelude.Nat | |
open import Prelude.Equality | |
open import Prelude.Product | |
open import Prelude.Unit | |
open import Prelude.Show | |
open import Prelude.String | |
open import Prelude.Semiring | |
This file contains 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
open import Prelude.Nat | |
open import Prelude.Equality | |
open import Prelude.Product | |
open import Prelude.Unit | |
open import Prelude.Show | |
open import Prelude.String | |
open import Prelude.Semiring | |
This file contains 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
open import Prelude.Nat | |
open import Prelude.Equality | |
open import Prelude.Product | |
open import Prelude.Unit | |
open import Prelude.Show | |
open import Prelude.Bool | |
open import Prelude.String | |
open import Prelude.Semiring | |
open import Prelude.Equality |
This file contains 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
module Magda where | |
--We need to model the agents that interact with the software. | |
-- , the world. | |
-- Each agent has specific material properties that make him better suited in specific computations | |
-- and specific material jobs. Thus agents need to have as type , a specific role of a system. | |
-- Roles have meaning inside specific organizational structures. or in other words the type of work performed and | |
-- the type of computation determines the roles that are needed, in a way that not one role can be taken apart and analyzed independently. |
This file contains 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
data K : Set where | |
WSet : Set₁ | |
WSet = K → Set | |
variable | |
HW HQ : WSet | |
This file contains 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
data Bool : Set where | |
true : Bool | |
false : Bool | |
data D : Set where | |
d : D | |
data E : Set where | |
e : E |