This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- | |
This file is intended for Lean beginners. The goal is to demonstrate what it feels like to prove | |
things using Lean and mathlib. Complicated definitions and theory building are not covered. | |
-/ | |
-- We want real numbers and their basic properties | |
import data.real.basic | |
-- We want to be able to define functions using the law of excluded middle | |
local attribute [instance, priority 0] classical.prop_decidable |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/bash | |
# script: time-docker-build.sh | |
# | |
# All command line arguments are passed to docker build command. | |
# | |
# usage: ./time-docker-build.sh | |
# | |
DATE_FORMAT="+%s" |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Delay a JS Promise by a number | |
// of miliseconds. Preserves arguments. | |
const delayPromise = (duration) => { | |
return (...args) => { | |
return new Promise((resolve, reject) => { | |
setTimeout(() => { | |
resolve(...args); | |
}, duration); | |
}); | |
}; |