Disco> :test x + 2 == 5
Error: there is nothing named x.
https://disco-lang.readthedocs.io/en/latest/reference/unbound.html
Disco> P : N -> Bool
Disco> P(x) = x + 2 == 5
Disco> :test P(3)
  - Certainly true: P(3)
Disco> :test P(2)
  - Certainly false: P(2)
Disco> -- A "proposition with input(s)" is called a *predicate*.
Disco> 
Disco> T : N * N -> Bool
Error: the shape of two types does not match.
https://disco-lang.readthedocs.io/en/latest/reference/shape-mismatch.html
Disco> TT : N * N -> Bool
Disco> TT(x,y) = x < y^2
Disco> TT(3,5)
T
Disco> :test TT(3,5)
  - Certainly true: TT(3, 5)
Disco> :test TT(3,3)
  - Certainly true: TT(3, 3)
Disco> :test TT(3,1)
  - Certainly false: TT(3, 1)
Disco> :test  forall n: N. P(n)
  - Certainly false: ∀n. P(n)
    Found counterexample:
      n = 0
Disco> :test forall n:N. n >= 0
  - Possibly true: ∀n. n >= 0
    Checked 100 possibilities without finding a counterexample.
Disco> :test forall b:Bool. (b /\ b) == b
  - Certainly true: ∀b. (b /\ b) == b
    No counterexamples exist; all possible values were checked.
Disco> :test forall n:Z. n >= 0
  - Certainly false: ∀n. n >= 0
    Found counterexample:
      n = -1
    - Left side:  -1
    - Right side: 0
Disco> :test forall p:Bool. (forall q:Bool. p /\ q == q /\ p)
  - Certainly false: ∀p. ∀q. p /\ q == q /\ p
    Found counterexample:
      p = F
      q = F
Disco> :test forall p:Bool. (forall q:Bool. (p /\ q) == (q /\ p))
  - Certainly true: ∀p. ∀q. (p /\ q) == (q /\ p)
    No counterexamples exist; all possible values were checked.
Disco> :doc P
P : ℕ → Bool
Disco> :defn P
P : ℕ → Bool
P(x) = x + 2 == 5
Disco> :test  exists n:N. P(n)
  - Certainly true: ∃n. P(n)
    Found example:
      n = 3
Disco> :test  exists n:N. P(n) /\ P(n+1)
  - Possibly false: ∃n. P(n) /\ P(n + 1)
    No example was found; checked 100 possibilities.
Disco> :test  exists n:N. exists r:N.  TT(n,r)
  - Certainly true: ∃n. ∃r. TT(n, r)
    Found example:
      n = 0
      r = 1
Disco> :test  exists n:N. exists r:N.  TT(n,r) /\ TT(n+1,r)
  - Certainly true: ∃n. ∃r. TT(n, r) /\ TT(n + 1, r)
    Found example:
      n = 0
      r = 2
Disco> :test forall n:N. exists m:N. n < m
  - Possibly true: ∀n. ∃m. n < m
    Checked 100 possibilities without finding a counterexample.
Disco> :test exists m:N. (forall n:N. n < m)
  - Possibly false: ∃m. ∀n. n < m
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. a^2 + b^2 == c^2
  - Certainly true: ∃a. ∃b. ∃c. a ^ 2 + b ^ 2 == c ^ 2
    Found example:
      a = 0
      b = 0
      c = 0
    - Left side:  0
    - Right side: 0
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> :test exists a:N. exists b:N. exists c:N. (a > 0) /\ (b > 0) /\ a^2 + b^2 == c^2
  - Possibly false: ∃a. ∃b. ∃c. a > 0 /\ b > 0 /\ a ^ 2 + b ^ 2 == c ^ 2
    No example was found; checked 100 possibilities.
Disco> 3^2 + 4^2 == 5^2
T
Disco>