Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
module Weed where
data : Set where
magic : {A : Set} A
magic ()
data Weed (A : Set) : Set where
grow : (A Weed A) Weed A
smoke : {A : Set} (P : Weed A Set)
(p : (f : A Weed A) (ih : (a : A) P (f a)) P (grow f))
(w : Weed A) P w
smoke P p (grow f) = p f λ a smoke P p (f a)
smokeout : {A : Set} A Weed A
smokeout a = smoke _ λ f ih ih a
weed-is-magic : {A B : Set} A Weed A B
weed-is-magic a w = magic (smokeout a w)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.