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 Coq #84

Closed tchajed closed 3 months ago

tchajed commented 3 months ago

Coq is an interactive theorem prover developed by INRIA. It's widely used for formalized mathematics, proving metaproperties of programming languages, and program proofs.

Coq is supported by linguist and has about 5k GitHub stars.

This is the syntax sample I wrote for shiki, as highlighted by GitHub:

From Coq Require Import ssreflect.

(* ensure proofs are well-structured *)
Set Default Goal Selector "!".
#[global] Open Scope general_if_scope.

Module list_playground.
  (* Let's do a typical proof by induction: we'll define [list] as an inductive,
     [app] (list append) as a recursive function, and prove that [app] is
     associative. *)
  Inductive list (A: Type) :=
  | nil
  | cons (x: A) (l: list A).

  (* Fix up implicit arguments. *)
  Arguments nil {A}.
  Arguments cons {A} x l.
  Notation "[]" := nil.
  Infix "::" := cons.

  Fixpoint app {A} (l1 l2: list A): list A :=
    match l1 with
    | [] => l2
    | x :: l1 => x :: app l1 l2
    end.

  Infix "++" := app.

  Theorem app_assoc {A} (l1 l2 l3: list A) :
    (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
  Proof.
    induction l1 as [|x l1]; simpl.
    - reflexivity.
    - by rewrite IHl1.
  Qed.
End list_playground.
netlify[bot] commented 3 months ago

Deploy Preview for textmate-grammars-themes ready!

Name Link
Latest commit 4383e7d8419ec6c4ef5e1330c92fbf1e98fa72a2
Latest deploy log https://app.netlify.com/sites/textmate-grammars-themes/deploys/66b641049d25510009448e31
Deploy Preview https://deploy-preview-84--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.