ncfavier

Require Import Arith ZArith Lia List Ascii String Program.Basics.
Open Scope string_scope.
Open Scope program_scope.
Import ListNotations.

(** The head character of a string, returned as a new string.
   If the string is empty, returns the empty string. *)

Definition head s := match s with
  | "" => ""

ncfavier

module Lib (shortestLongest) where

import Control.Applicative
import Data.Maybe

steps = go []
  where
    go l (x:xs) = Nothing : go (x:l) xs
    go l [] = Just [reverse l] : repeat (Just [])

ncfavier

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function.Base
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Sum

data Bin : Set where
  ⟨⟩ : Bin

ncfavier

open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import 1Lab.Type
open import 1Lab.Equiv

data Susp {ℓ} (A : Type ℓ) : Type ℓ where
  N S   : Susp A
  merid : A → N ≡ S

data Join {ℓ₁ ℓ₂} (A : Type ℓ₁) (B : Type ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where

ncfavier

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import Data.Bool

data Niltok : Type where
  t : Niltok
  nicht : Niltok → Niltok
  mod2 : (n : Niltok) → n ≡ nicht (nicht n)
  coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n)

ncfavier

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary

data ℤ : Type where

ncfavier

module LEM where

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.HLevel
open import 1Lab.HIT.Truncation
open import Data.Sum

⊥-is-prop : is-prop ⊥
⊥-is-prop ()

ncfavier

{ size ? 1000 }: with builtins;
let
  enumerate = genList (i: i + 1);
  sum = foldl' add 0;
  divides = n: k: n / k * k == n;
  factors = n: filter (divides n) (enumerate (n / 2));
  perfect = n: sum (factors n) == n;
in
filter perfect (enumerate size)

ncfavier

-- Moved to https://agda.monade.li/NatChurchMonoid.html

ncfavier

open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Relation.Binary.PropositionalEquality

Futamura projections

Let us represent programs from inputs I to outputs O as simple functions I → O, and assume we have a specialiser: a program that partially evaluates another program applied to the "static" part of its input.