This page is deprecated and superseded by https://ice1000.org/2020/05-04-ReplWithGoals.html.
λ> java -jar cli-1.3.0-full.jar -i
Arend REPL 1.3.0: https://arend-lang.github.io :? for help
λ \open Nat
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) |
#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 |
--- 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) |
#ifdef _MSC_VER | |
#pragma once | |
#endif | |
#ifndef LIST_HPP | |
#define LIST_HPP | |
#include <cstddef> | |
#include <iterator> | |
#include <initializer_list> |
{-# 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 |
{-# LANGUAGE LambdaCase #-} | |
data Term | |
= TmVar Integer | |
| TmAbs String Term | |
| TmApp Term Term | |
deriving (Show, Eq) | |
termShift :: Integer -> Term -> Term | |
termShift d = walk 0 |
\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 |
This page is deprecated and superseded by https://ice1000.org/2020/05-04-ReplWithGoals.html.
λ> java -jar cli-1.3.0-full.jar -i
Arend REPL 1.3.0: https://arend-lang.github.io :? for help
λ \open Nat
-- 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) |