Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/opaque-opaque.v

Created October 29, 2021 23:34
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Blaisorblade/231badd66f5018ebf161afe5adbb763e to your computer and use it in GitHub Desktop.
Save Blaisorblade/231badd66f5018ebf161afe5adbb763e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
opaque-opaque.v
From Coq Require Import Vector.
Lemma foo : nat.
Proof. exact 1. Qed.
Eval compute in foo.
Eval vm_compute in foo.
Lemma bar : nat.
Proof. exact 1. Defined.
Definition baz : Fin.t bar := Fin.F1.
Eval compute in bar.
Eval vm_compute in bar.
Eval compute in baz.
Opaque bar.
Eval compute in bar.
Eval vm_compute in bar.
(* [bar] is still definitionally equal to [1 : nat]. *)
Definition baz1 : Fin.t bar := baz.
Definition baz2 : Fin.t 1 := baz.
Eval compute in baz.
Eval vm_compute in baz.
Eval vm_compute in baz2.
(* [foo] is not definitionally equal to [1 : nat]. *)
(* Definitional equality is not there for foo! *)
Definition baz3 : Fin.t foo := baz.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment