Skip to content
Snippets Groups Projects
Commit 94a60883 authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Update some documentation

parent a030410e
No related branches found
No related tags found
No related merge requests found
......@@ -30,7 +30,7 @@ trait Expressions { self: Trees =>
}
}
/** Represents an expression in Leon. */
/** Represents an expression in Inox. */
abstract class Expr extends Tree with Typed
/** Trait which gets mixed-in to expressions without subexpressions */
......@@ -326,9 +326,6 @@ trait Expressions { self: Trees =>
}
/** $encodingof `... ==> ...` (logical implication).
*
* This is not a standard Scala operator, but it results from an implicit
* conversion in the Leon library.
*
* @see [[Constructors.implies]]
*/
......@@ -428,7 +425,7 @@ trait Expressions { self: Trees =>
*
* Division and Remainder follows Java/Scala semantics. Division corresponds
* to / operator on BigInt and Remainder corresponds to %. Note that in
* Java/Scala % is called remainder and the "mod" operator (Modulo in Leon) is also
* Java/Scala % is called remainder and the "mod" operator (Modulo in Inox) is also
* defined on BigInteger and differs from Remainder. The "mod" operator
* returns an always positive remainder, while Remainder could return
* a negative remainder. The following must hold:
......
......@@ -128,7 +128,7 @@ trait Paths { self: SymbolOps with TypeOps with Constructors =>
* within a fixpoint computation where the `ids` set is iteratively computed
* by performing [[filterByIds]] calls on some (unchaning) base [[Path]].
*
* @see [[leon.purescala.FunctionClosure.close]] for an example usecase.
* @see [[stainless.extraction.innerfuns.FunctionClosure.transform]] for an example usecase.
*/
def filterByIds(ids: Set[Identifier]): Path = {
def containsIds(ids: Set[Identifier])(e: Expr): Boolean = exprOps.exists {
......@@ -216,7 +216,7 @@ trait Paths { self: SymbolOps with TypeOps with Constructors =>
lazy val toClause: Expr = and(BooleanLiteral(true))
/** Like [[toClause]] but doesn't simplify final path through constructors
* from [[leon.purescala.Constructors]] */
* from [[Constructors]] */
lazy val fullClause: Expr = fold[Expr](BooleanLiteral(true), Let, And(_, _))(elements)
/** Folds the path into a boolean proposition where let-bindings are
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment