aymanosman

#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)

aymanosman

#lang pie

;; Exercises on Nat equality from Chapter 8 and 9 of The Little Typer

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (n m)

aymanosman

#lang pie

;; Exercises on ind-Nat from Chapter 10 of The Little Typer


;; Prelude

(claim +
  (-> Nat Nat Nat))
(define +

aymanosman

#lang pie

;; Prelude

(claim +
  (-> Nat Nat Nat))
(define +
  (lambda (n m)
    (rec-Nat n
      m

aymanosman

#lang pie

(claim =consequence
  (-> Nat Nat U))

(define =consequence
  (lambda (n m)
    (which-Nat n
      (which-Nat m
        Trivial

aymanosman

#lang pie

;; Exercises on Absurd from Chapter 15 of The Little Typer

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (a b)

aymanosman

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" \

aymanosman

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

#lang cur

(require cur/ntac/base
         cur/ntac/standard
         cur/ntac/rewrite
         cur/stdlib/sugar
         cur/stdlib/nat
         cur/stdlib/equality)

((ntac

aymanosman

#lang pie

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (a b)
    (rec-Nat a
      b