From 00fb0b9dee66a5ba012170c3313454934c976d5e Mon Sep 17 00:00:00 2001
From: Ryan Lahfa
Date: Wed, 17 Apr 2024 17:35:13 +0200
Subject: fix(backends/lean): extract more keywords from `lstlean.tex`

Taken from
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L33
and
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L36-L43.

This will not extract the tactics.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
---
 compiler/ExtractBase.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ddffb1c2..e30c4b36 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -916,6 +916,8 @@ let keywords () =
     | Lean ->
         [
           "Pi";
+          "Prop";
+          "Sort";
           "Type";
           "abbrev";
           "alias";
-- 
cgit v1.2.3