Skip to content

Instantly share code, notes, and snippets.

module F1
import System
import Data.Bool
import Data.List
import Data.Vect
import Decidable.Equality
data Fruit = Apple | Banana
module DecBool
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
where
fEf : False = False
fEf = Refl
import xml.dom.minidom
import sys
def traverse(e,o):
oldwhere = None
useo = dict(o.items())
if e.nodeType == e.TEXT_NODE:
return
@prozacchiwawa
prozacchiwawa / mood-dark-theme.el
Created March 10, 2021 02:38
Very hacky adaptation of an emacs dark theme for brighter, funner colors.
;;; mood-dark-theme.el - Coding palette based on atari 2600 colors. based on the following
;; emacs theme:
;; spacemax-common.el --- Color theme with a dark and light versions.
;; Copyright (C) 2019 Michael Camilleri
;; Author: Michael Camilleri
;; URL: <https://github.com/pyrmont/spacemax-theme>
;;
@prozacchiwawa
prozacchiwawa / macpaint-to-pgm.py
Created February 16, 2021 05:17
a twitter thread reminiscing about bbses pre-internet got me thinking about this. does a good enough job of converting old .mac
import sys
def shiftout(fout, bs):
for b in bs:
bb = b
for i in range(8):
if (bb >> 7) % 2 == 0:
fout.write(bytes([255]))
else:
fout.write(bytes([0]))
data SignedNat : Bool -> Nat -> Type where
Neg : (n:Nat) -> SignedNat True n
Pos : (n:Nat) -> SignedNat False n
data Memory : sna -> mem -> Type where
MWord : sna -> mem -> Memory sna mem
MEnd : sna -> Memory sna Void
data MemoryAddress : Nat -> Type where
MAddr : (n:Nat) -> MemoryAddress n
data SignedNat : Bool -> Nat -> Type where
Neg : (n:Nat) -> SignedNat True n
Pos : (n:Nat) -> SignedNat False n
interface MagnitudeSN sn where
magSN : sn -> Nat
implementation MagnitudeSN (SignedNat True Z) where
magSN _ = Z
module GLFW
-- https://gist.github.com/alrunner4/8a026f3bfea354b48d3294a20c9812e2
export data Monitor : Type where {}
export data Window : Type where {}
%foreign "C:glfwInit,libglfw"
Init: PrimIO Int
%foreign "C:glfwCreateWindow,libglfw"
@prozacchiwawa
prozacchiwawa / initialise.c.diff
Created September 20, 2020 04:37
WIP designated initialisers diff.
diff --git a/tdfc2/src/common/construct/initialise.c b/tdfc2/src/common/construct/initialise.c
index 4af7a0e0f..9a0c33ed8 100644
--- a/tdfc2/src/common/construct/initialise.c
+++ b/tdfc2/src/common/construct/initialise.c
@@ -6,9 +6,11 @@
*/
#include <stdio.h>
+#include <string.h>
@prozacchiwawa
prozacchiwawa / gist:fb9e072ba08092c92af65759fb9140a8
Created August 28, 2020 07:39
Attempt at describing the workflow for adding c99 features in tendra
<?xml version="1.0" standalone="no"?>
<!DOCTYPE chapter SYSTEM "minidocbook.dtd">
<chapter id="tdfc2-grammar-and-data-structure-notes">
<title>TDFC2: Working with the grammars and data structures to support new C99 features</title>
<section>
<title>Tools involved in adding C99 features</title>
<table>