TOTBWF

open import 1Lab.Prelude

open import Data.Bool
open import Data.Fin
open import Data.List
open import Data.Nat

module Data.Bool.CNF where

TOTBWF

#include <fcntl.h>
#include <immintrin.h>
#include <stdio.h>
#include <sys/mman.h>
#include <sys/stat.h>

uint32_t parse_4_digits(const __m128i input) {
  const __m128i char_0 = _mm_set1_epi8('0');

  // Normalize the '0' char to actually be 0x00.

TOTBWF

module 1Lab.Reflection.Duh where

open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat

private
  try-all : Term → Nat → Telescope → TC Term
  try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []

TOTBWF

(** Core Types *)
module Syntax =
struct
  type t =
    | Local of int
    | Hole of string
    | Let of string * t * t
    | Lam of string * t
    | Ap of t * t
    | Pair of t * t

TOTBWF

module NbE where

data Term
    = Var Int
    -- ^ DeBruijin Indicies (count outwards)
    | Lam Term
    | App Term Term
    | Pair Term Term
    | Fst Term
    | Snd Term

TOTBWF

{-# LANGUAGE TypeApplications #-}
module TwitterProblem where

import Data.SBV

--------------------------------------------------------------------------------
-- Complex Numbers, constructed from Algebraic Reals

data AlgComplex a = AlgComplex { real :: a, imaginary :: a}

TOTBWF

{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core
open import Categories.Category.Cartesian

module Categories.Tactic.Cartesian.Solver {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

open import Level

open import Categories.Category.BinaryProducts

TOTBWF

{-# OPTIONS --without-K --safe #-}
module Operads where

open import Level

open import Categories.Category.Core
open import Categories.Functor.Core

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; sym)
import Relation.Binary.PropositionalEquality as Eq

TOTBWF

{-# OPTIONS --without-K --safe #-}
module InitialAlgebra where

open import Level hiding (zero) renaming (suc to ℓ-suc)

open import Relation.Binary.PropositionalEquality.Core

open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.List.Base using (List; []; _∷_)

TOTBWF

{-# OPTIONS --allow-exec #-}

-- Embed a file as a string inside of an agda program.
-- To use this, make sure to add '/bin/cat' to '~/.agda/executables'

module Static where

open import Function

open import Data.Unit