arademaker

% git clone git@github.com:lecopivo/SciLean.git
Cloning into 'SciLean'...
remote: Enumerating objects: 21713, done.
remote: Counting objects: 100% (2158/2158), done.
remote: Compressing objects: 100% (861/861), done.
remote: Total 21713 (delta 1681), reused 1608 (delta 1267), pack-reused 19555 (from 3)
Receiving objects: 100% (21713/21713), 11.59 MiB | 5.75 MiB/s, done.
Resolving deltas: 100% (15628/15628), done.

ar@MacBook-Pro-14-2025 temp % cd SciLean

arademaker

import matplotlib.pyplot as plt
from wordcloud import WordCloud, STOPWORDS

# Sample text
with open('abstracts.txt', 'r') as f:
    text = f.read()

my = set(['multi', 'expressions','word', 'MWE'])
stops = set(STOPWORDS).union(my)

arademaker

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, [], [])

arademaker

fmod ATT is
 pr QID .
 
 sort Att .
 sort Constraint .

 op attrval : String Qid -> Att .
 op attrval : String String -> Att .
 
 op qeq : Qid Qid -> Constraint .

arademaker

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

arademaker

{-# LANGUAGE OverloadedStrings, DeriveGeneric #-}

module Annotation (readData) where

import Data.Aeson
    ( genericToJSON,
      object,
      encode,
      genericParseJSON,
      defaultOptions,

arademaker

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. ##

arademaker

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

arademaker

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),

arademaker

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