jozefg

Operator Russell : ().
[Russell] =def= [{x : U{i} | not(member(x; x))}].

Tactic break-plus {
  @{ [x : _ + _ |- _] => elim <x> }
}.

Theorem u-in-u-wf : [member(member(U{i}; U{i}); U{i'})] {
  unfold <member>; eq-eq-base; unfold <bunion>; auto;
  csubst [ceq(U{i}; lam(x.snd(x)) pair(inr(<>); U{i}))]

AndrasKovacs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

juliensagot

import SwiftUI

struct AquaScrollBar: View {
  @ScaledMetric private var height = 35.0
  
  var body: some View {
    Track()
      .frame(height: height)
      .overlay(alignment: .leading) {
        Thumb()