We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 3c4a9f4 commit 780ee54Copy full SHA for 780ee54
book/src/engine/major_concepts.md
@@ -9,9 +9,9 @@ logic.
9
A "goal" in Chalk can be thought of as "something we want to prove". The engine
10
itself understands `GoalData`s. `GoalData`s consist of the most basic logic,
11
such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`).
12
-On the other hand, `Goal` represents an opaque goal generated
+On the other hand, `DomainGoal` represents an opaque goal generated
13
externally. As such, it may contain any extra information or may be interned.
14
-When solving a logic predicate, Chalk will lazily convert `Goal`s
+When solving a logic predicate, Chalk will lazily convert `DomainGoal`s
15
into `GoalData`s.
16
17
There are three types of completely opaque `GoalData`s that Chalk can solve:
0 commit comments