bugaevc

#include <stdio.h>
#include <type_traits>
#include <utility>
#include <new>

template<typename T>
void forget1(T &&value) {
    union Forget {
        ~Forget() { }
        typename std::remove_reference<T>::type t;

bugaevc

bugaevc

import kotlinx.coroutines.channels.SendChannel
import kotlinx.coroutines.coroutineScope
import kotlinx.coroutines.flow.Flow
import kotlinx.coroutines.flow.channelFlow
import kotlinx.coroutines.flow.collectIndexed
import kotlinx.coroutines.launch
import kotlinx.coroutines.suspendCancellableCoroutine
import kotlinx.coroutines.sync.Mutex
import kotlinx.coroutines.sync.Semaphore
import java.util.*

bugaevc

import Lean

/--
`(h : a) ∧ b`, the "dependent and" connective. This is a conjunction
just like `And`, but to even state the right hand side proposition,
we need the left hand side to hold.
Due to proof irrelevance, this is not actually quite as dependent as
it might look.
-/
structure DAnd {a : Prop} (b : a → Prop) : Prop where

bugaevc

class Arrow (A : Type u → Type u → Type w) where
  comp (outer : A β γ) (inner : A α β) : A α γ
  ofFunction : (α → β) → A α β
  mapFirst : A α β → A (α × γ) (β × γ)

instance : Arrow (· → ·) where
  comp := Function.comp
  ofFunction := id
  mapFirst arrow | (a, g) => (arrow a, g)