pushd ../../raw
wc -l *.raw | awk '$1 < 6 {print $2}' > ../ner/wks/files.all
popd
jq -r '.[].name' documents.json | awk '{gsub(/txt/,"raw"); print}' > files.in
View test.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
section TEST | |
axiom x : Type | |
axiom e : Type | |
axiom _man_n_1 : x → Prop | |
axiom _walk_v_1 : e → x → Prop | |
-- a man is walking | |
def h1a : Prop := ∃ e2 x3, _man_n_1 x3 ∧ _walk_v_1 e2 x3 | |
def h1b : Prop := ∃ x3, _man_n_1 x3 ∧ ∃ e2, _walk_v_1 e2 x3 |
View processing.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE OverloadedStrings, DeriveGeneric #-} | |
module Annotation (readData) where | |
import Data.Aeson | |
( genericToJSON, | |
object, | |
encode, | |
genericParseJSON, | |
defaultOptions, |
View config.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains any messages produced by compilers while | |
running configure, to aid debugging if configure makes a mistake. | |
It was created by repp configure beta, which was | |
generated by GNU Autoconf 2.71. Invocation command line was | |
$ ./configure | |
## --------- ## | |
## Platform. ## |
View all-people.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
section | |
constant u : Type | |
-- constants from MRS | |
constant named : u → String → Prop | |
constant compound : u → u → u → Prop | |
constant _electronics_n_1 : u → Prop | |
constant _people_n_of : u → u → Prop | |
constant _go_v_1 : u → u → Prop | |
constant _to_p_dir : u → u → u → Prop |
View simple.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import tactic | |
example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := | |
begin | |
show_term { | |
intro h, | |
have ha := h.left, | |
have hbc := h.right, | |
cases hbc with hb hc, | |
exact or.inl (and.intro ha hb), |
View readme.org
View mathlibtoos.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
% pipx install mathlibtools | |
ERROR: Command errored out with exit status 1: | |
command: /Users/ar/.local/pipx/venvs/mathlibtools/bin/python -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-install-4zs2ysbb/pyyaml_c2e9947ee533476b87f4aeaa1aec081e/setup.py'"'"'; __file__='"'"'/private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-install-4zs2ysbb/pyyaml_c2e9947ee533476b87f4aeaa1aec081e/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' bdist_wheel -d /private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-wheel-6kj_k65w | |
cwd: /private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-install-4zs2ysbb/pyyaml_c2e9947ee533476b87f4aeaa1aec081e/ | |
Complete output (67 lines): | |
running bdist_wheel | |
running build | |
running build_py | |
creating build | |
creating build/lib.macosx-11-x86_64-3.9 |
View Merge.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DeriveGeneric, OverloadedStrings #-} | |
import qualified Data.ByteString.Lazy as B | |
import Data.List | |
import System.FilePath.Posix | |
import System.IO | |
import System.Environment | |
import Data.Aeson | |
import Data.Text | |
import GHC.Generics |
View merge.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Data.List | |
import System.FilePath.Posix | |
-- read the files into a list of strings (assuming they are an ordered list of pathnames) | |
-- convert the list of pathnames into a list of objs | |
-- merge the list of objs | |
-- produce the output | |
-- or http://hackage.haskell.org/package/multiset-0.2.2/docs/Data-MultiSet.html | |
line1 = "ontonotes-release-5.0/data/files/data/english/annotations/bc/cctv/00/cctv_0000.parse" |
View cipher.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Excerpt From: Graham Hutton. “Programming in Haskell.” | |
import Data.Char | |
positions :: Eq a => a -> [a] -> [Int] | |
positions x xs = [i | (x',i) <- zip xs [0..], x == x'] | |
lowers :: String -> Int | |
lowers xs = length [x | x <- xs, x >= 'a' && x <= 'z'] |
NewerOlder