Skip to content
Snippets Groups Projects
  1. Jul 19, 2022
    • SimonGuilloud's avatar
      Changed printer test. · 620f7056
      SimonGuilloud authored
      Now variables are always shown with a leading ? (except when following a binder)
      620f7056
    • SimonGuilloud's avatar
      Ran scalafmt · e8aa5ca8
      SimonGuilloud authored
      e8aa5ca8
    • SimonGuilloud's avatar
      Corrected eroneous proof. Created VariableFormulaLabel to replace arity-0 predicate schemas. · b401364e
      SimonGuilloud authored
      Any work on top of current LISA release should be easily adaptable by:
       - Changing all instances of Arity 0 SchematicFunctionLabel by VariableLabel
       - Changing all instances of Arity 0 SchematicPredicateLabel by VariableFormulaLabel
       - Changing all matching on SchematicFunctionLabel by either VariableLabel, SchematicFunctionLabel or SchematicTermLabel, according to whether the arity should be =0, >0 or >=0.
       - Changing all instances of multiary SchematicPredicateLabel by SchematicNPredicateLabel
       - Removing the empty parenthesis () that where used to transform an Arity 0 label to a term or formula. Variables have the implicit conversion without the call.
      b401364e
    • SimonGuilloud's avatar
      Changed the whole project to remove 0-arity schematic variables and replace... · eab5e80a
      SimonGuilloud authored
      Changed the whole project to remove 0-arity schematic variables and replace them by variables. It compiles, but at least one proof doesn't go through.
      eab5e80a
  2. Jun 24, 2022
  3. Jun 23, 2022
Loading