Skip to content

Commit

Permalink
add documentation for TesterType as a comment above the case class
Browse files Browse the repository at this point in the history
  • Loading branch information
FedericoAureliano authored and polgreen committed May 7, 2024
1 parent 3b6f2e7 commit 378e9bf
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions src/main/scala/uclid/lang/UclidLanguage.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1220,6 +1220,9 @@ case class ConstructorType(id: Identifier, inTypes: List[(Identifier, Type)], ou
override def isMap = true
}

// Every tester $t$ corresponds to exactly one constructor $c$ of an ADT inType.
// $t$ is a predicate that takes a term $x$ of type inType and returns true iff
// $x$ was built using constructor $c$.
case class TesterType(id: Identifier, inType: Type) extends Type {
override def toString = id + " " + inType.toString()
override def isMap = true
Expand Down

0 comments on commit 378e9bf

Please sign in to comment.