deemp

module A (P(..)) where
data P = MkP

deemp

"""
Creating a Kubernetes Deployment
"""
import pulumi
from pulumi_kubernetes.apps.v1 import Deployment, DeploymentSpecArgs
import pulumi_kubernetes.core.v1 as k8s
from pulumi_kubernetes.meta.v1 import ObjectMetaArgs, LabelSelectorArgs
from pulumi_kubernetes.provider import Provider
from pulumi import ResourceOptions

deemp

#lang rzk-1

-- A is contractible there exists x : A such that for any y : A we have x = y.
#def iscontr (A : U) : U
  := ∑ (a : A), (x : A) -> a =_{A} x

-- A is a proposition if for any x, y : A we have x = y
#def isaprop (A : U) : U
  := (x : A) -> (y : A) -> x =_{A} y

deemp

Light version

Works well when the maximum number of requests per 30 minutes can be sorted with 1 GB of RAM.

On each node, there is an FE and an MSD.
Nodes are indexed from 0 to 99.

MSD

Begin