analytic-bias

-- This file contains the code from the paper "Formalising
-- type-logical grammars in Agda", and was directly extracted from the
-- paper's source.
--
-- Note: because the symbol customarily used for the "left difference"
-- is unavailable in the Unicode character set, and the backslash used
-- for implication is often a reserved symbol, the source file uses a
-- different notation for the connectives: the left and right
-- implications are represented by the double arrows "⇐" and "⇒", and

analytic-bias

{
    "editor.fontSize": 16,
    "terminal.integrated.shell.windows": "C:\\WINDOWS\\Sysnative\\cmd.exe",
    "editor.wordWrap": "on",
    "latex-workshop.latex.tools": [
        {
            "name": "latexmk",
            "command": "latexmk",
            "args": [
                "-synctex=1",

analytic-bias

{"lastUpload":"2019-08-24T05:13:05.777Z","extensionVersion":"v3.4.2"}

analytic-bias

outputInBrainf''' :: String -> String
outputInBrainf''' s = do c <- s
                         replicate (ord c) '+' ++ ".>"

analytic-bias

module Codevs1080 where

import qualified Data.Vector as V; -- Use Vector for O(1) indexing

data Cmd = Add Int Int Int -- Order Index Addition
         | Inq Int Int Int -- Order Left-Index Right-Index
         deriving Show

logSolve :: [Int] -> [Cmd] -> [Int]
logSolve srcs cmds = V.toList addSum