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 / 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
% 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
@arademaker
arademaker / Merge.hs
Created October 31, 2020 20:59
Merge.hs
{-# 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