Skip to content

Instantly share code, notes, and snippets.

View Iainmon's full-sized avatar
🥶

Iain Moncrief Iainmon

🥶
View GitHub Profile
module Prim
import Data.Vect
import Data.Fin
-- import Data.Nat
-- import Data.List
-- %hide Prelude.cong
Require Import Coq.Init.Nat.
Inductive bit : Set := I | O.
Inductive bits : nat -> Set :=
| bnil : bits 0
| bcons : forall (n : nat), bit -> bits n -> bits (S n).
Arguments bcons [n] _ _.
@Iainmon
Iainmon / daniel3.v
Last active October 22, 2024 19:16
Require Import Unicode.Utf8.
Require Import Psatz.
Require Import Coq.Arith.Arith.
Require Import Coq.Init.Nat. (* needed? it seems no, with next line. *)
Import Nat.
Open Scope nat_scope.
Ltac save h1 h2 :=
(*pose proof h1 as h2*)
let t := type of h1 in
assert (h2 : t) by (exact h1).
Tactic Notation "save" constr(h1) "as" ident(h2) :=
save h1 h2.
(* Ltac replace_equivalent a b p :=
@Iainmon
Iainmon / daniel.v
Last active September 24, 2024 18:55
Lemma my_eq_sym: forall a b : Set, a = b -> b = a.
Proof.
intros a b.
intros H.
rewrite -> H || rewrite <- H.
reflexivity.
Qed.
Ltac inv H := inversion H; clear H; try subst.
module Ficu where
import Text.Parsec
( anyChar,
char,
noneOf,
oneOf,
between,
choice,
many1,
proc convShape() {}
iter regions(dom: domain(2,int), k: int, stride: int) {
const (h,w) = convShape(dom.shape,k,stride,padding=0);
for (i,j) in {0..#h,0..#w} {
yield dom[i * k * stride..#k,j * k * stride..#k];
}
}
@Iainmon
Iainmon / fibonacci.asm
Last active October 16, 2022 22:44
Fibonacci numbers in MASM
INCLUDE Irvine32.inc
; #define MAX_ITER 45
; int main() {
; int n;
; int m;
; int tmp;
; int i;
; i = 0;
; n = 0;
@Iainmon
Iainmon / Branch.hs
Last active September 11, 2022 06:23
import Control.Applicative ( Alternative(empty, (<|>)) )
newtype Branch s a = Branch (s -> [(a,s)])
branch :: (s -> [(a,s)]) -> Branch s a
branch = Branch
run :: Branch s a -> (s -> [(a,s)])
run (Branch f) = f
const float rt = sqrt(2.);
float anim(float speed) {
return (.5*sin(iTime * speed)) + 0.5;
}
const vec3 paint = vec3(0.17, 0.55, 0.70);
void mainImage( out vec4 fragColor, in vec2 fragCoord )