NathanHowell

🦾 Lean4 — ultra-condensed ref

🧠 Core: dep-TT (CIC); pure/strict FP; Curry–Howard; Sorts `Prop`/`Type u`/`Sort u`; Prop impredicative & proof-irrelevant; pipeline parse→macro→elab(cmd/term/tac)→kernel→IR/native; InfoTree/InfoView; Pratt parser; term-style vs `by` tactic-style.
🔤 Univ: levels u v w; `max/imax/succ`; cumulativity (Sort u↪Sort u+1); `Prop = Sort 0`; `Type u = Sort (u+1)`; Π typing→`Sort (imax i j)`; universe params `.{u}`; defeq β δ ζ ι η.
⛳ Binders & implicits: `(x:α)` explicit; `{x}` implicit; `⦃x⦄` strict-implicit; `[x:α]` instance-implicit; `_`/`?m` holes; casts `(e : T)`; `@f` exposes implicits; section/`variable` params auto-insert; implicit lambdas & named args.
🏗 Decls & recursion: `def`/`abbrev`/`opaque`/`theorem`/`lemma`/`example`/`axiom`; `unsafe`/`partial`/`noncomputable`; pattern-matching; structural & well-founded (`WellFounded.fix`) recursion; `mutual`; equation compiler; `termination_by`/`decreasing_by`/`wfRel`; `where` locals.
📦 Modules & scope: file `A/B/C.lean`≡`A.B.C`; `prelu

NathanHowell

load("@io_bazel_rules_docker//container:providers.bzl", "BundleInfo", "ImageInfo")
load("//deployment/docker:image_name.bzl", "image_name")
load(":providers.bzl", "DigestInfo", "RepoInfo")

def _bundle_impl(target, ctx):
    bundle_info = target[BundleInfo]
    return RepoInfo(image_digests = {
        image_name(bundle_info, x[ImageInfo]): x[DigestInfo]
        for x in ctx.rule.attr.image_targets
    })

NathanHowell

FROM alpine@sha256:ddba4d27a7ffc3f86dd6c2f92041af252a1f23a8e742c90e6e1297bfa1bc0c45 AS build
RUN apk add --no-cache ca-certificates curl python3
ARG CLOUD_SDK_VERSION=280.0.0
RUN curl https://dl.google.com/dl/cloudsdk/channels/rapid/downloads/google-cloud-sdk-${CLOUD_SDK_VERSION}-linux-x86_64.tar.gz \
      | tar xzf -

RUN /google-cloud-sdk/install.sh \
      --bash-completion=false \
      --override-components beta pubsub-emulator \
      --path-update=false \

NathanHowell

load("@io_bazel_rules_docker//container:bundle.bzl", "container_bundle")
load("@io_bazel_rules_docker//container:image.bzl", "container_image")
load("@io_bazel_rules_docker//contrib:push-all.bzl", _push_bundle = "docker_push")

container_image(
    name = "my_first_image",
    ...
)

container_image(

NathanHowell

load("@rules_python//python:defs.bzl", "py_runtime", "py_runtime_pair")
load(":venv.bzl", "py_venv")
load(":wrapper.bzl", "py_wrapper")

py_venv(
    name = "py3_venv",
    # caching the venv interpreter doesn't work for two reasons:
    #
    # * there are no platform dependencies on this target: the cache will contain binaries for the wrong OS
    # * there are no dependencies on the interpreter binary or standard library: the cache may contain stale versions

NathanHowell

// find all build.gradle files in the expected locations in the build tree
fileTree('.')
    .matching {
      exclude '**/src/**', '**/build/**', '**/.*'
      include '**/build.gradle'
    }
    .each {
      // then convert the file path to a project path
      final relative = rootProject.projectDir.relativePath(it.parentFile)
      final project = ":${relative.replace('/', ':')}"

NathanHowell

/*
 * Licensed to the Apache Software Foundation (ASF) under one
 * or more contributor license agreements.  See the NOTICE file
 * distributed with this work for additional information
 * regarding copyright ownership.  The ASF licenses this file
 * to you under the Apache License, Version 2.0 (the
 * "License"); you may not use this file except in compliance
 * with the License.  You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0

NathanHowell

Keybase proof

I hereby claim:

• I am nathanhowell on github.
• I am nathanhowell (https://keybase.io/nathanhowell) on keybase.
• I have a public key ASC5cgtZMOLRHjV1qLg1TtuAv8xI1wjwmwqhvv9eUn7ybAo

To claim this, I am signing this object:

NathanHowell

FROM alpine:3.6 AS base
RUN apk add --no-cache python3 ca-certificates tzdata tini \
 && apk upgrade --no-cache

FROM base AS build
RUN apk add --no-cache \
      python3-dev \
      cython \
      build-base

NathanHowell

import tensorflow as tf
from scipy.special import logit


def centering_inference(c):
    """
    :param c: the number of target classes
    :return: a uniformly distributed class bias variable
    """
    return tf.Variable(