Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extract definitions/theorems of functions, add Sigma and Pi #222

Merged
merged 9 commits into from
Oct 8, 2024

Conversation

shilangyu
Copy link
Contributor

Slimmed down SetTheory a bit, should make it easier to find theorems.

For reviewing: The first commit is moving existing things to the new package, the following commits are newly added things.

Comment on lines +296 to +310
// class SetOfFunctions(val x: Term, val y: Term) extends AppliedFunctional(setOfFunctions, Seq(x, y)) with LisaObject[SetOfFunctions] {
// override def substituteUnsafe(map: Map[lisa.fol.FOL.SchematicLabel[?], lisa.fol.FOL.LisaObject[?]]): SetOfFunctions = SetOfFunctions(x.substituteUnsafe(map), y.substituteUnsafe(map))

// override def toString(): String = x.toStringSeparated() + " |=> " + y.toStringSeparated()
// override def toStringSeparated(): String = toString()
// }
// object SetOfFunctions {
// def unapply(sof: SetOfFunctions): Option[(Term, Term)] = sof match
// case AppliedFunctional(label, Seq(x, y)) if label == setOfFunctions => Some((x, y))
// case _ => None
// }
// extension (x: Term) {
// // Infix notation for a set of functions: x |=> y
// def |=>(y: Term): Term = SetOfFunctions(x, y)
// }
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is one regression: in the type package |=> was used as the setOfFunctions, but it was declared as an infix which gave nicer printing. I tried to replicate this here but I failed. The with LisaObject[SetOfFunctions] part was raising an error of Type argument lisa.maths.settheory.functions.Functionals.SetOfFunctions does not conform to upper bound Common.this.LisaObject[lisa.maths.settheory.functions.Functionals.SetOfFunctions]

Copy link
Collaborator

@SimonGuilloud SimonGuilloud left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

@SimonGuilloud SimonGuilloud merged commit 70cc576 into epfl-lara:main Oct 8, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants