Revision: 06.08.2023, https://compute.toys/view/407
fn sdSphere(p: vec3f, r: f32) -> f32 {
return length(p) - r;
}
import Mathlib | |
open Lean Meta Elab Command | |
-- generalized | |
/-- Write an import graph, represented as a an array of `NameMap`s to the ".dot" graph format. | |
If `("style1", graph1)` is in `graphs`, then the edges in `graph1` will be labeled with `[style1]`. | |
Example: `asStyledDotGraph #[("", graph1), ("style=dashed", graph2)]` -/ | |
def asStyledDotGraph [ForIn Id α Name] (graphs : Array (String × NameMap α)) | |
(header := "import_graph") : String := Id.run do |
#!/bin/bash | |
# | |
# Container source: https://github.com/OpenAccess-AI-Collective/axolotl/blob/main/docker/Dockerfile-runpod | |
# | |
# | |
# To run this in RunPod with `winglian/axolotl-runpod:main-cu118-2.0.0`, set | |
# Expose HTTP Ports (Max 10): 7860,8888 | |
# docker command: `bash -c "curl -H 'Cache-Control: no-cache' https://raw.githubusercontent.com/utensil/llm-playground/main/scripts/entry/prepare_ax.sh -sSf | bash"` | |
# JUPYTER_PASSWORD change to your secret | |
# HUGGINGFACE_TOKEN change to your token from https://huggingface.co/settings/tokens |
Revision: 06.08.2023, https://compute.toys/view/407
fn sdSphere(p: vec3f, r: f32) -> f32 {
return length(p) - r;
}
Use https://github.com/jfarley248/iTunes_Backup_Reader
git clone https://github.com/jfarley248/iTunes_Backup_Reader
cd iTunes_Backup_Reader
# apply https://github.com/jfarley248/iTunes_Backup_Reader/pull/12
gh pr checkout https://github.com/jfarley248/iTunes_Backup_Reader/pull/12
https://www.nerdfonts.com/font-downloads
The following solution thanks to @hackerzgz & @snacky101 will install all nerd fonts;
brew tap homebrew/cask-fonts
brew search '/font-.*-nerd-font/' | awk '{ print $1 }' | xargs -I{} brew install --cask {} || true
import data.finsupp | |
namespace finsupp.eric | |
#check finset.sigma | |
universes u v w | |
def bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α → finset β) : finset (α × β) | |
:= (sa.sigma fb).map (equiv.sigma_equiv_prod _ _).to_embedding |
import data.dfinsupp | |
import tactic | |
universes u v w | |
variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj] | |
variables (β : ii → jj → Type w) [Π i j, decidable_eq (β i j)] | |
variables [Π i j, has_zero (β i j)] | |
def to_fun (x : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j := |
-- A One-Line Proof of the Infinitude of Primes | |
-- [The American Mathematical Monthly, Vol. 122, No. 5 (May 2015), p. 466] | |
-- https://twitter.com/pickover/status/1281229359349719043 | |
import data.finset.basic -- for finset, finset.insert_erase | |
import data.nat.prime -- for nat.{prime,min_fac} and related lemmas | |
import data.real.basic -- for real.nontrivial, real.domain | |
import analysis.special_functions.trigonometric -- for real.sin and related identities | |
import algebra.big_operators -- for notation `∏`, finset.prod_* | |
import algebra.ring -- for domain.to_no_zero_divisors |
In this tutorial I'll show you how to create a Github webhook that will post updates from your Github account to a channel in Discord. The steps are simple so follow along!
First you need to create a webhook in a text channel. We're assuming you have both Manage Channel
and Manage Webhooks
permissions!