louisswarren

data ⊥ : Set where

hmm : ∀ α → ⊥
-- Agda infers that
--   α : ⊥
-- because that's only way this could be provable?
hmm α = α

louisswarren

{-# LANGUAGE EmptyDataDecls, EmptyCase, ExistentialQuantification,
             ScopedTypeVariables, NoMonomorphismRestriction, Rank2Types,
             PatternSynonyms #-}
module MAlonzo.Code.Qfasttail where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, eqFloat, add64, sub64,
                    mul64, quot64, rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text

louisswarren

open import Agda.Builtin.Bool

data ⊥ : Set where
record ⊤ : Set where

isTrue : Bool → Set
isTrue true = ⊤
isTrue false = ⊥

data ℕ : Set where

louisswarren

def cast(f):
    returns = f.__annotations__['return']
    if callable(returns):
        casters = returns,
    else:
        casters = reversed(returns)
    def inner(*args, **kwargs):
        r = f(*args, **kwargs)
        for caster in casters:
            r = caster(r)

louisswarren

def returnlater(f):
    def inner(*args, **kwargs):
        x = f(*args, **kwargs)
        r = None
        while True:
            try:
                r = next(x)
            except StopIteration as final:
                if final.value is not None:
                    return final.value

louisswarren

open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_-_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality

data ⊥ : Set where

infix 3 ¬_
¬_ : (A : Set) → Set
¬ A = A → ⊥

louisswarren

open import Agda.Builtin.Sigma

open import Decidable
open import List

module Third (Ω : Set) (_≟_ : Decidable≡ Ω) where

data Filter {A : Set} (P : Pred A) : List A → List A → Set where
  []   : Filter P [] []
  _∷_  : ∀{x xs ys} → P x    → Filter P xs ys → Filter P (x ∷ xs) (x ∷ ys)

louisswarren

-- agda 2.5.99.20181017-9

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Fin : ℕ → Set where

louisswarren

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

data ⊥ : Set where

¬_ : Set → Set
¬ P = P → ⊥

Surjective : {A B : Set} → (A → B) → Set

louisswarren

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

data ⊥ : Set where

¬_ : Set → Set
¬ P = P → ⊥

Surjective : {A B : Set} → (A → B) → Set