rntz

import Data.List

interface Cat obj (0 hom: obj -> obj -> Type) where
  id : {a: obj} -> hom a a
  seq: {a, b, c: obj} -> hom a b -> hom b c -> hom a c

interface Cat (List obj) hom => Concat obj hom where
  para: {Γ₁, Γ₂, Δ₁, Δ₂ : List obj}
     -> hom Γ₁ Δ₁ -> hom Γ₂ Δ₂ 
     -> hom (Γ₁ ++ Γ₂) (Δ₁ ++ Δ₂)

rntz

from talon import Module, Context, actions
from typing import Any, NamedTuple, Union, Optional
from dataclasses import dataclass
import logging

mod = Module()
ctx = Context()

# Types.
Motion = Union[str, tuple]

rntz

#lang racket

(require syntax/parse/define)

;; steps:
;; 1. defining the category structure
;; 2. typechecking/elaborating into morphisms


;;; ---------- CATEGORICAL STRUCTURE ----------

rntz

# please don't commit this to user repos, it uses unstable talon APIs - in
# particular, the audio metadata.
from talon import speech_system
import logging

# ignore all phrase recognitions that take fewer than this many ms.
IGNORE_THRESHOLD = 100

# name: (bad_threshold, worse_threshold)
# you probably want to modify these for your computer & usage patterns.

rntz

from talon import Module, Context, actions

mod = Module()
ctx = Context()
subtitles_enabled = None

def update_subtitles(state):
    global subtitles_enabled
    subtitles_enabled = state
    if subtitles_enabled is not None:

rntz

from talon import Module, Context, actions

mod = Module()
ctx = Context()

matching_delimiters = {x[0]: x[1] for x in "() [] {} <> “” ‘’".split()}

mod.list('delimiter', desc='Delimiter pair names')
ctx.lists['self.delimiter'] = {
    "round": "(", "square": "[", "curly": "{", "angle": "<",

rntz

mode: dictation
-
^command$:
  mode.disable("dictation")
  mode.enable("command")
^command [mode|mood|boat] <phrase>$:
  mode.disable("dictation")
  mode.enable("command")
  user.rerun_phrase(phrase)

rntz

search:
    edit.find()
    user.quick_macro_set("edit.find_next")

go next | later:
    edit.find_next()
    user.quick_macro_set("edit.find_next")

go last | prior:
    edit.find_previous()

rntz

@mod.action_class
class Actions:
    def welcome_back():
        "Wakes talon up."
        logging.info("Waking Talon up.")
        actions.user.mouse_wake()
        actions.user.history_enable()
        actions.user.talon_mode()

    def sleep_all():

rntz

fib :: Int -> Int
fib 0 = 1
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

data Type = IntType | StringType deriving (Eq, Show)
data Expr = IntExpr Int
          | StringExpr String
          | PlusExpr Expr Expr
          | IntToString Expr