Small fixes about "fst", "snd", and "pair" functions. New logo. Comments in the code.
New welformedness checks and fixes.
- Checks wether all variables in the right part of a macro are in the left part or public.
- Checks wether all variable in the right part of an equation are in the left part.
- Provides a quick fix for function names again with editing distance.
- Checks wether built-ins are imported to use corresponding functions or symbols (provides a quick fix to import the right built-in).
- Editing distance is now used to display all close tokens (distance < 3) and not the first one only.
diff
is considered as a reserved function symbol so that there is no error while using it.- Functions with arity 0 may be used without parenthesis.
Fix package.json
Initial release after fork from giclu-3.
-
Enhances giclu-3's syntax highlighting.
-
Adds comprehensive syntax error detection based on the grammar with
MISSING
orERROR
messages. -
Provides various wellformedness checks:
- Checks position and usage of reserved facts (
Fr
,Out
,In
,K
,KD
,KU
). - Checks whether variable are used consistly inside a rule, i.e., using the same capitalization and sort.
- Spellcheck on facts (must start with an uppercase letter).
- Checks whether all variables in the conclusion of a rule appear in the premises (except public variables).
- Checks the arity of facts and functions.
- Checks whether a lemma uses free terms.
- Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).
- Checks position and usage of reserved facts (
-
Use right click and
Rename
on an indentifier to rename all occurences of it inside a rule or a lemma. -
Use right click and
Search Definition
on facts or function names and pressCTRL
+TAB
to navigate through all occurences.