emilyhorsman

module Termination where

open import Data.Maybe
open import Data.Sum

data Unit : Set where
  unit : Unit

record Stream : Set where
  coinductive

emilyhorsman

*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.

emilyhorsman

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

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
       

emilyhorsman

# 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

emilyhorsman

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

emilyhorsman

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]

emilyhorsman

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);
}

emilyhorsman

uint8_t byteRead;
uint8_t byteIndex;
uint8_t checksum;
uint8_t buttonNum;
bool buttonVal;
bool validState;

void loop() {
  t = millis();

emilyhorsman

Axiom “Demo”: Q ⇒ P

Theorem “Contrapositivity is the antitonicity of logical not”: ¬ P ⇒ ¬ Q
Proof:
    ¬ P
  ⇒⟨ “Contrapositive” with “Demo” ⟩
    ¬ Q