ntabee

-- https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#exercises
open classical

variables p q r s : Prop

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) := 
assume (h: p -> r ∨ s),
by_cases (
  assume hp: p,
  have hrs: r ∨ s, from h hp,

ntabee

-- https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#exercises

variables p q r : Prop

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := 
  ⟨ assume h: p ∧ q, ⟨h.right, h.left⟩, assume h: q ∧ p, ⟨h.right, h.left⟩ ⟩

example : p ∨ q ↔ q ∨ p := 
  ⟨

ntabee

#/bin/sh

# 1. Place wslpath (https://gist.github.com/ntabee/d7af5686dc4a99fda5a77b4ef081b102) in /usr/local/bin (or anywhere path-aware)
# 2. Place this script in "C:\Program Files\Microsoft VS Code Insiders\bin"
# 3. chmod a+x both scripts.

set +x
SCRIPTDIR=`dirname "$0"`
SCRIPTDIR=`wslpath -w -r "${SCRIPTDIR}"`
EXE="${SCRIPTDIR}\\..\\Code - Insiders.exe"

ntabee

#!/bin/bash

# This is free and unencumbered software released into the public domain.
#
# Anyone is free to copy, modify, publish, use, compile, sell, or
# distribute this software, either in source code form or as a compiled
# binary, for any purpose, commercial or non-commercial, and by any
# means.
#
# In jurisdictions that recognize copyright laws, the author or authors

ntabee

#include <array>
#include <iostream>
#include "tempra.hpp"

template<unsigned n, typename R>
struct print_randoms {
    static void print() {
        typedef typename Next<R>::type RND;
        std::cout << RND::value << std::endl;
        print_randoms<n-1, RND>::print();