shikijs / textmate-grammars-themes

Collection of TextMate grammars and themes in JSON
https://textmate-grammars-themes.netlify.app/
MIT License
116 stars 57 forks source link

feat: add support for Lean #69

Closed ydewit closed 4 months ago

ydewit commented 4 months ago

Lean is a functional programming language and interactive theorem prover developed by Microsoft Research. It bridges the gap between automated and interactive theorem proving, supporting both mathematical reasoning and general-purpose programming.

Key features of Lean include:

Here's a sample of Lean code to demonstrate the syntax:

import Mathlib.Tactic

-- Define a simple function
def double (n : Nat) : Nat := 2 * n

-- Prove a simple theorem
theorem double_zero : double 0 = 0 := by
  rw [double, Nat.mul_zero]

-- Define an inductive type
inductive Tree (α : Type)
  | leaf : α → Tree α
  | node : Tree α → Tree α → Tree α

-- Pattern matching on the Tree type
def treeSize {α : Type} : Tree α → Nat
  | Tree.leaf _ => 1
  | Tree.node l r => treeSize l + treeSize r + 1

-- Use a tactic block for a more complex proof
theorem treeSize_positive {α : Type} (t : Tree α) : treeSize t > 0 := by
  induction t with
  | leaf _ => simp [treeSize]; exact Nat.zero_lt_one
  | node l r ihl ihr => 
    simp [treeSize]
    exact Nat.lt_trans ihl (Nat.lt_add_right _ _ _)

#eval double 21  -- Evaluates to 42
netlify[bot] commented 4 months ago

Deploy Preview for textmate-grammars-themes ready!

Name Link
Latest commit 20e0e94a093d779340ad5d63321c1529b505d964
Latest deploy log https://app.netlify.com/sites/textmate-grammars-themes/deploys/669026f575f4b20007b9e3b7
Deploy Preview https://deploy-preview-69--textmate-grammars-themes.netlify.app
Preview on mobile
Toggle QR Code...

QR Code

Use your smartphone camera to open QR code link.

To edit notification comments on pull requests, go to your Netlify site configuration.

ydewit commented 4 months ago

I cannot see lean as part of the languages in the playground: https://deploy-preview-69--textmate-grammars-themes.netlify.app/ Although I could see it in my local playground.

cireu commented 3 months ago

hello, I'm using Shiki for Lean4 highlight and I found the line comment highlight is broken. Do you have any ideas?

(The picture is taken from https://shiki.style/)

图片