Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/leaky_strings.v

Last active July 19, 2022 21:43
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/1806e5da72be8d751f89baed85bd58bd to your computer and use it in GitHub Desktop.
Save Blaisorblade/1806e5da72be8d751f89baed85bd58bd to your computer and use it in GitHub Desktop.
Download ZIP
Coq strings are so logical, they're literally built on truth
Raw
leaky_strings.v
Require Import iris.proofmode.proofmode.
Lemma string_fun (PROP : bi) (X : PROP) : X ⊢ X.
Proof.
iIntros "X".
generalize true; intros.
Show.
(*
1 goal
PROP : bi
X : PROP
b : bool
============================
String (Ascii.Ascii false false false b b false b false) "" :
X
--------------------------------------∗
X
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment