Skip to content

Instantly share code, notes, and snippets.

@ratmice

ratmice/gist:ae54d9b27f7afa8cabb7cc84c42550e0

Created August 1, 2022 13:44
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 ratmice/ae54d9b27f7afa8cabb7cc84c42550e0 to your computer and use it in GitHub Desktop.
Save ratmice/ae54d9b27f7afa8cabb7cc84c42550e0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
-- From the post https://dylanj.xyz/posts/rust-coq-opaque-types/
-- Figured it would be fun to do a lean version without tactics.
def impl_trait_transform (Trait: Type → Prop) (Result: Prop) :
((∃ t, Trait(t)) → Result) ↔ (∀ t, (Trait(t) → Result)) :=
⟨λ existsTrait, λ ty, λ trait, existsTrait ⟨ty, trait⟩,
λ anyTrait, λ existsTrait, exists.elim existsTrait (λ ty, anyTrait ty)⟩
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment