search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

instantiatePredicateSchemas does not instantiates VariableFormulaLabels #80

Closed lighthea closed 1 year ago

lighthea commented 1 year ago

instantiatePredicateSchemas does not instantiates VariableFormulaLabels despite taking SchematicVarOrPredLabel as arguments of its substitution map. Can be reproduced with :


val a = VariableFormulaLabel("a")
val b = VariableFormulaLabel("b")

isSame(instantiatePredicateSchemas(a(), Map(a -> LambdaTermFormula(Seq(), b()))), a() )
SimonGuilloud commented 1 year ago

Solved in https://github.com/epfl-lara/lisa/pull/83