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 pandas as pd | |
# Load the data | |
df = pd.read_excel('pnas.2118631119.sd01.xlsx') | |
import matplotlib.pyplot as plt | |
# Filter the data for ages 22-35 | |
df_filtered = df[(df['AGE'] >= 22) & (df['AGE'] <= 35) & (df['YEAR'] >= 1955) & (df['YEAR'] <= 2040)] |
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 pandas as pd | |
# Load the Supplementary Data S1 from the lead poisoning PNAS paper | |
# https://www.pnas.org/doi/full/10.1073/pnas.2118631119 | |
df = pd.read_excel('pnas.2118631119.sd01.xlsx') | |
# Load the Supplementary Data S1 from the ADDM/CDDS paper | |
# https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6223814/ | |
file_path_s1 = 'autism_S1.xls' | |
autism_s1 = pd.read_excel(file_path_s1) |
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 pandas as pd | |
# Load the data | |
df = pd.read_excel('pnas.2118631119.sd01.xlsx') | |
from bs4 import BeautifulSoup | |
# Load the HTML file | |
with open('crime.html', 'r') as f: | |
contents = f.read() |
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
-- warning: this is hacky. run at your own risk. | |
-- | |
-- before you run this, put sum_list.asm in a dynamic library. | |
-- | |
-- on OSX that means | |
-- $ nasm -f macho64 sum_list.asm | |
-- $ libtool -dynamic sum_list.o -o libsum_list.dylib | |
-- | |
-- on Linux it means | |
-- $ nasm -f elf64 sum_list.asm |
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
Parameter set : Set. | |
Parameter In : (set * set) -> Prop. | |
Definition subset (A B : set) : Prop := | |
forall x : set, In(x,A) -> In(x,B). | |
Axiom ZF_extensionality : | |
forall X Y : set, | |
(forall z : set, In(z,X) <-> In(z,Y)) | |
-> X = Y. |
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
#![feature(test)] | |
mod expr_adt { | |
pub enum Expr { | |
Var(String), | |
Const(f64), | |
Plus(Box<Expr>, Box<Expr>), | |
Times(Box<Expr>, Box<Expr>), | |
} | |
pub fn gen_evaluator<'a, F : 'a + Fn(&str) -> f64> (env: F) -> Box<dyn 'a + Fn(&Expr) -> f64> { |
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
Require Import Arith Decidable Euclid Psatz Wf_nat. | |
Definition divides a b := exists k, b = k * a. | |
Definition prime p := 2 <= p /\ forall k, divides k p -> (k = 1 \/ k = p). | |
Lemma dec_divides k n: decidable (divides k n). | |
Proof with intuition. | |
case (le_gt_dec k 0)... | |
- case (le_gt_dec n 0). | |
+ left; exists 0... |
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
Require Import Coq.Lists.List Coq.Relations.Relations Coq.Sorting.Sorted. | |
Require Import Coq.Program.Equality Psatz. | |
Lemma Sorted_iff_by_explicit_indices {A} {R: relation A} (l: list A): | |
Sorted R l <-> forall n, (S n) < length l -> exists d, | |
R (nth n l d) (nth (S n) l d). | |
Proof with (cbn in *; firstorder). | |
split; induction l; intros. | |
- unshelve esplit; contradict H0... | |
- unshelve esplit; intuition; inversion H. |
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
Require Import Coq.Lists.List Coq.Logic.Eqdep. | |
Definition vec (A: Type) (n: nat) : Type := {l: list A | length l = n}. | |
Section vec_rev. | |
Variable A : Type. | |
Variable n : nat. | |
Definition vec_rev (l: vec A n): vec A n. | |
Proof. | |
refine (exist _ (rev (proj1_sig l)) _). |
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
// Reference implementation of combinatory algebra | |
#include <stdio.h> | |
#include <stdlib.h> | |
struct term { | |
enum { | |
ATOM_S, | |
ATOM_K, | |
ATOM_I, |
NewerOlder