Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/gist:327a9c466e3aaecf38fe93109ef8fde6

Last active June 2, 2018 03:00
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 kbuzzard/327a9c466e3aaecf38fe93109ef8fde6 to your computer and use it in GitHub Desktop.
Save kbuzzard/327a9c466e3aaecf38fe93109ef8fde6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
import data.nat.prime
namespace nat
definition Prime := subtype prime
-- unit test
definition two' : Prime := ⟨2,prime_two⟩
instance Prime_is_nat : has_coe Prime ℕ := ⟨subtype.val⟩
-- unit test
example : (two' : ℕ) = 2 := rfl
end nat
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment