File: algebra_finite.v

package info (click to toggle)
coq-iris 4.4.0-2
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 4,196 kB
  • sloc: python: 130; makefile: 62; sh: 34; sed: 2
file content (11 lines) | stat: -rw-r--r-- 414 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
 
From iris.algebra Require Import ofe stepindex_finite.

(** Test that [decide] finds the instance for [Nat], not [SIdx.eq_dec]. *)
Goal ∀ n1 n2 : nat, decide (n1 = n2) = Nat.eq_dec n1 n2.
Proof. done. Qed.

Goal ∀ (A : ofe) n (x1 x2 : later A), Next x1 ≡{n}≡ Next x2.
Proof.
  intros A n x1 x2. f_contractive_fin.
  Show. (* Goal should be [x1 ≡{n}≡ x2], not [x1 ≡{n'}≡ x2] with [n' < n] *)
Abort.