bvis

pipeline {
    agent { node { label 'swarm-ci' } }

    environment {
        TEST_PREFIX = "test-IMAGE"
        TEST_IMAGE = "${env.TEST_PREFIX}:${env.BUILD_NUMBER}"
        TEST_CONTAINER = "${env.TEST_PREFIX}-${env.BUILD_NUMBER}"
        REGISTRY_ADDRESS = "my.registry.address.com"

        SLACK_CHANNEL = "#deployment-notifications"

TakashiHarada

module AgdaBasics where

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true

myuon

infix 4 _∈_ _∉_
data _∈_ {f} {A : Set f} (x : A) (B : Set f) : Set (suc f) where
  in-eq : A ≡ B → x ∈ B

_∉_ : {B : Set} → B → Set → Set₁
X ∉ A = (X ∈ A) → ⊥

module elem-lemmas where
  elem-∈ : {A B : Set} → ∀{x : B} → x ∈ A → A
  elem-∈ {x = x} (in-eq ≡-refl) = x