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

#ifdef _MSC_VER
#pragma once
#endif

#ifndef LIST_HPP
#define LIST_HPP

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

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

#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

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

struct Config { blabla };
typedef int ConfigType;
enum ConfigType_ { Type1, Type2, Type3, TypeCOUNT; };

auto SetConfig(ConfigType type, Config config) -> void {
 switch (type) {
  case Type1: blablba; break;
  case Type2: blablba; break;
  case Type3: blablba; break;
  default: error(); break;

ice1000

operator fun <A, B, C> ((B) -> A).plus(p: (C) -> B) = { it: C -> this(p(it)) }

fun main(args: Array<String>) {
	val a: (Int) -> String = { it.toString() }
	val b: (String) -> ByteArray = { it.toByteArray() }
	println((b + a)(233))
	val c: (ByteArray) -> List<Int> = { it.map { it.toInt() } }
	println((c + b + a)(666)) // Haskell: c . b . a $ 666
}

ice1000

package main

/**
 * Created by ice1000 on 2017/5/2.
 *
 * @author ice1000
 */

fun main(args: Array<String>) {
	fun lambda(it: Int): Int =

ice1000

package main

/**
 * Created by ice1000 on 2017/4/27.
 *
 * @author ice1000
 */

fun <A, B, C : Any> zipWith(op: (A, B) -> C) = { x: Sequence<A> ->
	{ y: Sequence<B> ->

ice1000

import java.awt.BorderLayout
import java.awt.Color
import java.awt.Graphics
import java.io.File
import javax.swing.JFrame
import javax.swing.JPanel
import javax.swing.WindowConstants

/**
 * Created by ice1000 on 2017/3/18.