Skip to content
Avatar
🦅
I want to apply for a Ph.D.
🦅
I want to apply for a Ph.D.
  • 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
2.3k followers · 416 following · 521

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. JetBrains/Arend

    The Arend Proof Assistant

    Java 430 21

  2. agda/agda

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

    Haskell 1.3k 169

  3. pest-parser/intellij-pest

    pest grammar file support for all JetBrains IDEs

    Kotlin 25 3

  4. agda/cubical

    An experimental library for Cubical Agda

    Agda 190 56

  5. owo-lang/narc-rs

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

    Rust 46 2

  6. resume

    👾 My resume / 我的简历

    TeX 409 141

2,666 contributions in the last year

Sep Oct Nov Dec Jan Feb Mar Apr May Jun Jul Aug Mon Wed Fri
Learn how we count contributions.
Less
More

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.