Skip to content

Instantly share code, notes, and snippets.

🦈
The avatar is me

Tesla Ice Zhang‮ ice1000

🦈
The avatar is me
Block or report user

Report or block ice1000

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View infnat.agda
{-# 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
View linked_list_incomplete.hpp
#ifdef _MSC_VER
#pragma once
#endif
#ifndef LIST_HPP
#define LIST_HPP
#include <cstddef>
#include <iterator>
#include <initializer_list>
@ice1000
ice1000 / Printf.agda
Created Aug 7, 2018
Type safe printf
View Printf.agda
--- 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
ice1000 / ImRotateDemo.cpp
Last active Jul 29, 2018 — forked from carasuca/ImRotateDemo.cpp
Rotating text and icon demo for dear imgui
View ImRotateDemo.cpp
#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
ice1000 / Wow.agda
Created Jun 14, 2018
Some easy proves
View Wow.agda
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)
View Wtf.cpp
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;
View FunctionComposition.kt
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
ice1000 / kotlin-lambda-rec.kt
Created May 2, 2017
Kotlin can also write recursive lambda
View kotlin-lambda-rec.kt
package main
/**
* Created by ice1000 on 2017/5/2.
*
* @author ice1000
*/
fun main(args: Array<String>) {
fun lambda(it: Int): Int =
@ice1000
ice1000 / point-free.kt
Last active Apr 27, 2017
A Point-Free function implementation in Kotlin
View point-free.kt
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
ice1000 / displaying-fib-matrix-output-as-function.kt
Created Mar 29, 2017
This program displays the output of fib-matrix mentioned in my blog
View displaying-fib-matrix-output-as-function.kt
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.
You can’t perform that action at this time.