Skip to content

Instantly share code, notes, and snippets.

Emily Horsman emilyhorsman

Block or report user

Report or block emilyhorsman

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View Termination.agda
module Termination where
open import Data.Maybe
open import Data.Sum
data Unit : Set where
unit : Unit
record Stream : Set where
View sprintf.lagda
*Note*: I will call this ~sprintf~ instead of ~printf~ since we are not dealing with IO.
I will use the terminology from the [[][man page for ~sprintf~]].
~sprintf~ takes a "format string" which is any number of "directives".
A directive is either a character other than ~'%'~ or a "conversion specification" consisting of a ~'%'~ and conversion specifier (such as ~d~ for integers).
The design chosen during lecture failed since our level of abstraction was at characters instead of directives.
For instance, the string ~"%d"~ has two characters but only a single directive: the integer conversion specification.
We can start with a data type to represent directives.
View BirdPromotions.agda
open import Relation.Binary.PropositionalEquality renaming (refl to definition-chasing)
open ≡-Reasoning
open import Agda.Builtin.String
open import Function
defn-chasing : {i} {A : Set i} (x : A) String A A
defn-chasing x reason supposedly-x-again = supposedly-x-again
syntax defn-chasing x reason xish = x ≡⟨ reason ⟩′ xish
infixl 3 defn-chasing
emilyhorsman /
Last active Feb 10, 2019
Literate Agda in Org mode documents

Literate Agda in Org mode documents

Note: These instructions will be unnecessary after Agda 2.6.0 is released.

PR agda/adga#3548.

  1. Clone the Agda repository.
    git clone
    cd agda
# Abstract Data Type
class PointT:
def __init__(self, x, y):
self.__point = (x, y)
# sum : PointT -> R
# sum is an instance method.
# It acts on one instance.
# In Python we call an instance an object.
# An object from the class PointT is an object
View alternating_bools.agda
open import Data.Bool
open import Relation.Binary.PropositionalEquality renaming (refl to definition-chasing)
record List (A : Set) : Set where
-- Explicitly coinductive.
-- The fields of this record are the destructors of this coinductive type.
-- Notice: /No/ cons!
car : A
View Rose.hs
instance Arbitrary a => Arbitrary (Rose a) where
arbitrary =
numChildren :: Gen Int
numChildren = (`mod` 6) . abs <$> arbitrary
makeRose :: Arbitrary a => Int -> Gen (Rose a)
makeRose n = rose $ n `div` 2
branch :: Arbitrary a => Int -> Gen [Rose a]
TEST_CASE("Refraction straight through center from outside") {
Vec3f rayDirection({ 0, 0, -1 });
Vec3f normal({ 0, 0, 1 });
bool isTotalInternalReflection;
Vec3f refraction = refractionDir(rayDirection, normal, 1.2f, isTotalInternalReflection);
REQUIRE(refraction[0] == 0);
REQUIRE(refraction[1] == 0);
REQUIRE(refraction[2] == -1);
View BluetoothStateMachine.cpp
uint8_t byteRead;
uint8_t byteIndex;
uint8_t checksum;
uint8_t buttonNum;
bool buttonVal;
bool validState;
void loop() {
t = millis();
View Contrapositivity is the antitonicity of logical not
Axiom “Demo”: Q ⇒ P
Theorem “Contrapositivity is the antitonicity of logical not”: ¬ P ⇒ ¬ Q
¬ P
⇒⟨ “Contrapositive” with “Demo” ⟩
¬ Q
You can’t perform that action at this time.