TOTBWF

(** {1 Syntax} *)

(** Expressions. *)
type expr =
  | Var of cont * int
  (** Local references.

      Thorin is a "blockless" IR, so we can reference arguments of
      other nodes by adding a data dependency edge, which implicitly
      nests the two nodes. *)

TOTBWF

description
Segal conditions.

TOTBWF

module Blog.BCO where

TOTBWF

description
Inversion hell.

TOTBWF

description
Dialectica categories, done representably. June 4th, 2024 at the HIM trimester.

TOTBWF

description
Idempotent systems.

open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning
import Cat.Functor.Reasoning

TOTBWF

A short, self-contained proof that List A has UIP if A has UIP

First, we enable the --without-K flag, which removes UIP as an axiom. We also import Agda.Primitive, which gives us access to the Level type, though this isn't strictly required. We also add a variable block so we don't need to constantly abstract over types and levels.

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

TOTBWF

{-# OPTIONS --lossy-unification #-}
open import Cat.Prelude

open import Data.List
open import Data.List.Member
open import Data.Sum

open import Theories.Signature

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.