feat: add support for Lean (#69)

samples/lean.sample

@@ -0,0 +1,128 @@
+structure Point (α : Type u) where
+  mk :: (x : α) (y : α)
+  deriving Repr
+
+#check Point       -- a Type
+#check @Point.rec  -- the eliminator
+#check @Point.mk   -- the constructor
+#check @Point.x    -- a projection
+#check @Point.y    -- a projection
+
+#eval Point.x (Point.mk 10 20)
+#eval Point.y (Point.mk 10 20)
+
+open Point
+
+example (a b : α) : x (mk a b) = a :=
+  rfl
+
+example (a b : α) : y (mk a b) = b :=
+  rfl
+
+def p := Point.mk 10 20
+
+def Point.smul (n : Nat) (p : Point Nat) :=
+  Point.mk (n * p.x) (n * p.y)
+
+def xs : List Nat := [1, 2, 3]
+def f : Nat → Nat := fun x => x * x
+
+#eval xs.map f  -- [1, 4, 9]
+
+
+structure MyStruct where
+    {α : Type u}
+    {β : Type v}
+    a : α
+    b : β
+
+#check { a := 10, b := true : MyStruct }
+
+
+structure Point (α : Type u) where
+  x : α
+  y : α
+  z : α
+
+structure RGBValue where
+  red : Nat
+  green : Nat
+  blue : Nat
+
+structure RedGreenPoint (α : Type u) extends Point α, RGBValue where
+  no_blue : blue = 0
+
+def p : Point Nat :=
+  { x := 10, y := 10, z := 20 }
+
+def rgp : RedGreenPoint Nat :=
+  { p with red := 200, green := 40, blue := 0, no_blue := rfl }
+
+example : rgp.x   = 10 := rfl
+example : rgp.red = 200 := rfl
+
+
+class Add (a : Type) where
+  add : a → a → a
+
+instance [Add a] : Add (Array a) where
+  add x y := Array.zipWith x y (· + ·)
+
+instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
+  default := (default, default)
+
+
+#print inferInstance
+
+def foo : Inhabited (Nat × Nat) :=
+  inferInstance
+
+theorem ex : foo.default = (default, default) :=
+  rfl
+
+structure Rational where
+  num : Int
+  den : Nat
+  inv : den ≠ 0
+
+instance : OfNat Rational n where
+  ofNat := { num := n, den := 1, inv := by decide }
+
+instance : ToString Rational where
+  toString r := s!"{r.num}/{r.den}"
+
+#eval (2 : Rational) -- 2/1
+
+#check (2 : Rational) -- Rational
+#check (2 : Nat)      -- Nat
+
+class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hMul : α → β → γ
+
+export HMul (hMul)
+
+@[default_instance]
+instance : HMul Int Int Int where
+  hMul := Int.mul
+
+local instance : Add Point where
+  add a b := { x := a.x + b.x, y := a.y + b.y }
+
+attribute [-instance] addPoint
+
+namespace Point
+
+scoped instance : Add Point where
+  add a b := { x := a.x + b.x, y := a.y + b.y }
+
+def double (p : Point) :=
+  p + p
+
+end Point
+
+open Classical
+noncomputable scoped
+instance (priority := low) propDecidable (a : Prop) : Decidable a :=
+  choice <| match em a with
+    | Or.inl h => ⟨isTrue h⟩
+    | Or.inr h => ⟨isFalse h⟩

sources-grammars.ts

@@ -690,6 +690,12 @@ export const sourcesCommunity: GrammarSource[] = [
     aliases: ['kql'],
     source: 'https://github.com/rosshamish/kuskus/blob/master/kusto-syntax-highlighting/syntaxes/kusto.tmLanguage.json',
   },
+  {
+    name: 'lean',
+    aliases: ['lean4'],
+    source: 'https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json',
+    categories: ['general'],
+  },
   {
     name: 'liquid',
     displayName: 'Liquid',