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

FrozenWinters

` ------------------------------------------------
` Kevin Carlson, Astra Kolomatskaia, Reed Mullanix
` Narya formalisation of Kan complexes
`
` developed 13-18 May 2024 during the
`   Prospects of Formal Mathematics
` trimester program at the
`   Hausdorff Institute for Mathematics
`
` dated 7 June 2024

juliensagot

import SwiftUI

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