Skip to content

Instantly share code, notes, and snippets.

@aymanosman
aymanosman / show-how-equality-induction-works.rkt
Created Mar 5, 2020
There seams to be subtle differences between how the two inductive principles are set up in Coq vs Pie
View show-how-equality-induction-works.rkt
#lang pie
(claim +
(-> Nat Nat
Nat))
(define +
(λ (a b)
(rec-Nat a
b
View use-cur-example.rkt
#lang cur
(require cur/ntac/base
cur/ntac/standard
cur/ntac/rewrite
cur/stdlib/sugar
cur/stdlib/nat
cur/stdlib/equality)
((ntac
@aymanosman
aymanosman / App.nested-stack.js
Created Feb 10, 2020
react-navigation-stack ModalPresentationIOS with nested stacks
View App.nested-stack.js
import * as React from 'react';
import {View, Text, Button} from 'react-native';
import {NavigationNativeContainer} from '@react-navigation/native';
import {createStackNavigator, TransitionPresets} from '@react-navigation/stack';
function HomeScreen({navigation}) {
return (
<View style={{flex: 1, alignItems: 'center', justifyContent: 'center'}}>
<Text>Home Screen</Text>
<Button
@aymanosman
aymanosman / codesign.sh
Created Jan 3, 2020 — forked from Bogdanp/codesign.sh
Codesigning a Racket executable for inclusion in a macOS app
View codesign.sh
codesign --force \
--timestamp \
--entitlements="$CODE_SIGN_ENTITLEMENTS" \
--sign="$EXPANDED_CODE_SIGN_IDENTITY_NAME" \
-o runtime \
"${PROJECT_DIR}/Resources/core/lib/Racket.framework/Versions/7.5_3m/Racket"
codesign --force \
--timestamp \
--entitlements="$CODE_SIGN_ENTITLEMENTS" \
View chapter-15-Absurd.rkt
#lang pie
;; Exercises on Absurd from Chapter 15 of The Little Typer
(claim +
(-> Nat Nat
Nat))
(define +
(λ (a b)
View chapter-15.rkt
#lang pie
(claim =consequence
(-> Nat Nat U))
(define =consequence
(lambda (n m)
(which-Nat n
(which-Nat m
Trivial
View inequality.rkt
#lang pie
;; Prelude
(claim +
(-> Nat Nat Nat))
(define +
(lambda (n m)
(rec-Nat n
m
View ind-List.rkt
#lang pie
;; Exercises on ind-Nat from Chapter 10 of The Little Typer
;; Prelude
(claim +
(-> Nat Nat Nat))
(define +
@aymanosman
aymanosman / equality-Nat.rkt
Last active Feb 21, 2019
equality-Nat.rkt
View equality-Nat.rkt
#lang pie
;; Exercises on Nat equality from Chapter 8 and 9 of The Little Typer
(claim +
(-> Nat Nat
Nat))
(define +
(λ (n m)
@aymanosman
aymanosman / list-elimination.rkt
Last active Jan 23, 2019
The Little Typer: Exercises for Chapters 4 and 5
View list-elimination.rkt
#lang pie
;; Exercises on Pi types and using the List elimiator from Chapters 4 and 5
;; of The Little Typer
;;
;; Some exercises are adapted from assignments at Indiana University
(claim elim-Pair
(Π ((A U)
(D U)
You can’t perform that action at this time.