This file contains hidden or 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
module F1 | |
import System | |
import Data.Bool | |
import Data.List | |
import Data.Vect | |
import Decidable.Equality | |
data Fruit = Apple | Banana |
This file contains hidden or 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
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 |
This file contains hidden or 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 xml.dom.minidom | |
import sys | |
def traverse(e,o): | |
oldwhere = None | |
useo = dict(o.items()) | |
if e.nodeType == e.TEXT_NODE: | |
return |
This file contains hidden or 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
;;; 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> | |
;; |
This file contains hidden or 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 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])) |
This file contains hidden or 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
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 |
This file contains hidden or 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
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 |
This file contains hidden or 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
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" |
This file contains hidden or 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
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> | |
This file contains hidden or 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
<?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> |