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
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
def split [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)] | |
: List a → (a × List a × List a) | |
| [] => (default, [], []) | |
| x :: xs => | |
let rec op x acc := | |
if x ≤ acc.1 | |
then (x, acc.1 :: acc.2.2, acc.2.1) | |
else (acc.1, x :: acc.2.2, acc.2.1) | |
xs.foldr op (x, [], []) |
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
fmod ATT is | |
pr QID . | |
sort Att . | |
sort Constraint . | |
op attrval : String Qid -> Att . | |
op attrval : String String -> Att . | |
op qeq : Qid Qid -> Constraint . |
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 |
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, |
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. ## |
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 |
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), |
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 |
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 |
NewerOlder