Pinned Repositories
FormalMath
A side project about formalization of mathematics.
GridMaze-Algorithm
Description of the algorithms used in my app GridMaze
H-99
My solutions to "Ninety-Nine Haskell Problems"
Lambda-Calculus
An introduction to lambda calculus in Chinese, including an interpreter in Haskell.
polylink
A Blender Addon
Project-Euler
Solutions for Project Euler
Regular-Polytopes
Notes about Coxeter's "Regular Polytopes"
Surreal-Number
My note and programs about surreal number created by John Horton Conway
Symmetries-of-Things
Notes about "The Symmetries of Things"
txyyss's Repositories
txyyss/Lambda-Calculus
An introduction to lambda calculus in Chinese, including an interpreter in Haskell.
txyyss/FormalMath
A side project about formalization of mathematics.
txyyss/polylink
A Blender Addon
txyyss/Project-Euler
Solutions for Project Euler
txyyss/GridMaze-Algorithm
Description of the algorithms used in my app GridMaze
txyyss/H-99
My solutions to "Ninety-Nine Haskell Problems"
txyyss/Surreal-Number
My note and programs about surreal number created by John Horton Conway
txyyss/Symmetries-of-Things
Notes about "The Symmetries of Things"
txyyss/EmacsSettings
My Emacs Settings
txyyss/Regular-Polytopes
Notes about Coxeter's "Regular Polytopes"
txyyss/cdf-mech-sem
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
txyyss/company-coq
A Coq IDE build on top of Proof General's Coq mode
txyyss/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
txyyss/Hyperbolic-Tiling
Introduction and Code about Hyperbolic Tilings
txyyss/LovePoints
Animations for Valentine's Day
txyyss/omega
txyyss/PG
This repo is the new home of Proof General
txyyss/tron-legacy-emacs-theme
Original retro-futuristic theme inspired by Tron: Legacy
txyyss/VST
Verified Software Toolchain