zoeyfyi

module Main (main) where

import Agda.Compiler.Backend (Backend (..), Backend' (..), Recompile (Recompile), callBackend, setTCLens)
import Agda.Compiler.Common (IsMain (..))
import Agda.Interaction.BasicOps (atTopLevel)
import Agda.Interaction.FindFile (SourceFile (..))
import Agda.Interaction.Imports (CheckResult (..), Mode (..), parseSource, typeCheckMain)
import Agda.Interaction.Options qualified as A (defaultOptions)
import Agda.Syntax.Abstract.Name qualified as A (ModuleName, QName (..))
import Agda.Syntax.Internal qualified as A (Name (..))

pyrocto

# 
METHOD: TABLE
ENCODE: Unicode
PROMPT: TeX 1.13
VERSION: 1.13
DELIMITER: ,
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
TERMINPUTKEY: 
BEGINCHARACTER
alpha	α

AndrasKovacs

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

{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.

Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:

sandello

// Ivan Pouzyrevsky, EWSCS'12.

#include <iostream>
#include <functional>
#include <memory>
#include <utility>

// This is a C++ implementation for Seemingly Impossible Functional Program, which in finite time tests whether 
// a computable predicate on binary strings yields True for some binary string. It does so by exhaustive search
// on whole space. Some nasty-nasty tricks like call-by-need can make this algorithm run fast.