Skip to content
Avatar
🦅
I want to apply for a Ph.D.
🦅
I want to apply for a Ph.D.

Highlights

  • Arctic Code Vault Contributor
  • Pro

Organizations

@agda @JuliaEditorSupport @pest-parser @EmmyLua @ice1k @devkt-plugins @owo-lang @arend-lang
ice1000/README.md

Hi there 👋 I go by Tesla Ice Zhang. Typical usernames include ice1000 or tizusa.

Pinned

  1. The Arend Proof Assistant

    Java 430 21

  2. Agda is a dependently typed programming language / interactive theorem prover.

    Haskell 1.3k 169

  3. pest grammar file support for all JetBrains IDEs

    Kotlin 25 3

  4. An experimental library for Cubical Agda

    Agda 190 56

  5. (WIP) Dependently-typed programming language with Agda style dependent pattern matching

    Rust 46 2

  6. 👾 My resume / 我的简历

    TeX 409 141

Contribution activity

August 2020

Created an issue in JetBrains/Arend that received 2 comments

Infix FQN

For instance, we may want f `A.b` g. We can't do this yet, but it doesn't seem hard.

2 comments
10 contributions in private repositories Aug 2 – Aug 24

Seeing something unexpected? Take a look at the GitHub profile guide.

You can’t perform that action at this time.