ice1000

module Wow where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Binary.Core
open import Function
open import Relation.Nullary

-- lemma₁ : ∀ a b → (suc (a + suc a) ≡ suc (b + suc b)) → (a + a ≡ b + b)

ice1000

#include "imgui_internal.h"

int rotation_start_index;

auto ImRotateStart() -> void {
	rotation_start_index = ImGui::GetWindowDrawList()->VtxBuffer.Size;
}

auto ImRotationCenter() -> ImVec2 {
	ImVec2 l{FLT_MAX, FLT_MAX}, u{-FLT_MAX, -FLT_MAX}; // bounds

ice1000

--- http://ice1000.org/gist/safe-printf-agda/
module Printf where

open import Data.List using (List; _∷_; [])
open import Data.Char renaming (Char to ℂ)
open import Data.Nat using (ℕ; _+_)
open import Data.Nat.Show renaming (show to showℕ)
open import Data.Empty
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (yes; no)

ice1000

#ifdef _MSC_VER
#pragma once
#endif

#ifndef LIST_HPP
#define LIST_HPP

#include <cstddef>
#include <iterator>
#include <initializer_list>

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

data ω : Type₀ where

ice1000

{-# LANGUAGE LambdaCase #-}

data Term
    = TmVar Integer
    | TmAbs String Term
    | TmApp Term Term
    deriving (Show, Eq)

termShift :: Integer -> Term -> Term
termShift d = walk 0

ice1000

\data Bool1 | tt1 | ff1 \where {
  \func to2 (b : Bool1) : Bool2
    | tt1 => Bool2.tt2
    | ff1 => Bool2.ff2
  \lemma lemma (b : Bool1) : Bool2.to1 (to2 b) = b
    | tt1 => idp
    | ff1 => idp
}
\data Bool2 | tt2 | ff2 \where {
  \func to1 (b : Bool2) : Bool1

ice1000

REPLs with Typed Holes

This page is deprecated and superseded by https://ice1000.org/2020/05-04-ReplWithGoals.html.

Arend

λ> java -jar cli-1.3.0-full.jar -i
Arend REPL 1.3.0: https://arend-lang.github.io   :? for help
λ \open Nat

ice1000

A collection of ASCII art for "Arend"

... that doesn't look crazy to me.

Speed

_______                   _________
___    |________________________  /
__ /| |_ ___/ _ \_ __ \ __ / 

ice1000

-- twitter thread: https://twitter.com/EgbertRijke/status/1349865209591173120

{-# OPTIONS --cubical #-}

open import Cubical.HITs.PropositionalTruncation using (∥_∥; ∣_∣; squash; rec)
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Function using (_∘_; idfun)
open import Cubical.Data.Sigma using (_×_; fst; snd)
import Cubical.Data.Empty as ⊥ using (elim)