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
coinductive
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 [[https://linux.die.net/man/3/fprintf][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
emilyhorsman / Instructions.org
Last active Feb 10, 2019
Literate Agda in Org mode documents
View Instructions.org

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 https://github.com/agda/agda.git
    cd agda
        
View TutorialJan30.py
# 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!
coinductive
field
car : A
View Rose.hs
instance Arbitrary a => Arbitrary (Rose a) where
arbitrary =
let
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]
View RefractionUnitTests.cc
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);
REQUIRE(!isTotalInternalReflection);
}
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
Proof:
¬ P
⇒⟨ “Contrapositive” with “Demo” ⟩
¬ Q
You can’t perform that action at this time.