lambdageek

Sometimes I want to put an array inside of a mathpartir inferrule.

The straightforward thing doesn't work:

\begin{equation*}
\inferrule{Conclusion}{
  Premiss 1 \and
  \begin{array}{ll}
 1 & 2 \\ % note, this is where the problem happens

fgoinai

fun <T: Comparable<T>> eWhen(target: T, tester: Tester<T>.() -> Unit) {
    val test = Tester(target)
    test.tester()
    test.funFiltered?.invoke() ?: return
}

class Tester<T: Comparable<T>>(val it: T) {
    var funFiltered: (() -> Unit)? = null

    infix fun Boolean.then(block: () -> Unit) {

philard

String className = (this != null) ? this.getClass().getSimpleName() : "";
int wavFilesCount = new java.io.File("sounds").listFiles().length;
int clipIndex  = (className.hashCode() & 0x7FFFFFFF) % wavFilesCount;

javax.sound.sampled.Clip clip = javax.sound.sampled.AudioSystem.getClip();
java.io.File wavFile = new java.io.File("sounds" + java.io.File.separator + "sound" + clipIndex + ".wav");
javax.sound.sampled.AudioInputStream audio = javax.sound.sampled.AudioSystem.getAudioInputStream(wavFile);
clip.open(audio);
clip.start();

jespercockx

{-
======================================
=== THE GREAT RESURRECTION OF PROP ===
======================================

Bringing back the impredicative sort Prop of definitionally proof-irrelevant propositions to Agda.

To check this file, get the prop-rezz branch of Agda at https://github.com/jespercockx/agda/tree/prop-rezz.

This file is a short demo meant to show what you currently can (and can't) do with Prop.

fgoinai

from functools import partial, reduce
from itertools import chain
from typing import Callable, Any, Sequence, Optional, Mapping


class FnChain:
    """
    FnChain(obj).map(...).filter(...).reduce(...)...

    API LIST:

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

bobatkey

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

AndrasKovacs

{-# language LambdaCase, Strict, BangPatterns, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

module UnivPoly where

import Data.Foldable
import Data.Maybe
import Data.String
import Debug.Trace

Gabriella439

I'm writing this post to publicly come out as trans (specifically: I wish to transition to become a woman).

This post won't be as polished or edited as my usual posts, because that's kind of the point: I'm tired of having to edit myself to make myself acceptable to others.

I'm a bit scared to let people know that I'm trans, especially because I'm not yet in a position where I can transition (for reasons I don't want to share, at least not in public) and it's really shameful. However, I'm getting really

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3