Skip to content

Instantly share code, notes, and snippets.

View arademaker's full-sized avatar
🎯
Focusing

Alexandre Rademaker arademaker

🎯
Focusing
View GitHub Profile
@arademaker
arademaker / sciLean.txt
Created April 7, 2025 14:34
error in the SciLean build
% git clone [email protected]: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
arademaker / abstracts.py
Last active March 10, 2025 14:04
wordcloud of the keywords
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
arademaker / split.lean
Created December 4, 2024 16:53
split proof reduction size
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
arademaker / teste.maude
Last active May 2, 2024 21:44
from MRS Prolog to Maude for rewriting
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
arademaker / test.lean
Last active April 22, 2023 19:19
formal semantics example
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
arademaker / processing.hs
Created January 3, 2023 12:51
a Haskell code for parsing a json-lines file apply a simple transformation and serialize a simplified version
{-# LANGUAGE OverloadedStrings, DeriveGeneric #-}
module Annotation (readData) where
import Data.Aeson
( genericToJSON,
object,
encode,
genericParseJSON,
defaultOptions,
@arademaker
arademaker / config.log
Created August 9, 2022 13:57
config.log from repp compilation
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
arademaker / all-people.lean
Last active July 30, 2022 00:29
lean proof
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
arademaker / simple.lean
Created February 26, 2021 16:43
simple proof in Lean and show_term
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
arademaker / readme.org
Last active February 25, 2021 02:18
simple data work
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