Banus

Math input method in Mac OS X

This is a guide to map combinations of characters to Unicode mathematical symbols. The original inspiration is the incredibly useful gist by Andrej Bauer, and this gist aims to extend the idea to lower / upper case key combinations. This is achieved by using .cin input maps, originally developed to quickly insert Chinese characters, to encode a wide range of math symbols.
The method is expressive enough to encode almost all shortcuts from the keymap used by the Lean 4 plugin in Visual Studio Code.

Setup

1. Download the lean4.cin file from this repository or generate an up-to-date version by running the generate_cin.py script.   Don't copy-paste it from the browser because the file must be in UTF-8 encoding.

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 (..))

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.