ice1000

package org;
// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
// Use of this source code is governed by the GNU GPLv3 license that can be found in the LICENSE file.

import java.util.*;
import java.util.stream.Collectors;


/**
 * @author danihao123

ice1000

\newcommand{\lrbracket}[1]{\llbracket #1 \rrbracket}
\newcommand{\Tm}[2]{\text{Tm}(#1, #2)}
\newcommand{\FF}{\mathcal F}
\newcommand{\CC}{\mathcal C}
\newcommand{\EE}{\mathcal E}
\newcommand{\lrangle}[1]{\langle#1\rangle}
\newcommand{\Prop}{\text{Prop}}
\newcommand{\El}[1]{\text{El}(#1)}
\newcommand{\eqlzSimp}{\mathrm{eq}}
\newcommand{\eqlz}[2]{\eqlzSimp(#1,#2)}

ice1000

import java.util.List;
import java.util.Map;
public class Main {
	interface Level {
		// Pattern matcher
		interface Visitor<P, R> {
			R visitConst(Const c, P p);
			R visitInfinity(P p);
			R visitRef(Reference r, P p);
		}

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.HITs.S1

SInt : Type₀
SInt = base ≡ base

ice1000

{- Lean 4
open list
#eval filter (= 4) [1, 2, 4]
-}

open import Data.Nat renaming (ℕ to Nat; _≟_ to decEqNat)
open import Data.List using (List; []; _∷_)
open import Data.Bool using (true; false)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

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)

ice1000

A collection of ASCII art for "Arend"

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

Speed

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

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

\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

{-# LANGUAGE LambdaCase #-}

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

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