QDB: Quote #311618
About / Browse / Latest / Random / Queue / Prefs / Submit Quote / Search

This quote has been fermenting for 19 days and has been voted on 4 times.
Based on preliminary voting, this quote has a 30.6% chance of being approved.

#311618* (?/4) ⚐Flag
<@nsnc> crowell is doing nothing, therefore crowell is doing.
<@Maczilla-> Induction is so nice
<@bt> Induction is not doing Allah is doing
<@aweinstock> Allah_ind = fun (P : Allah -> Prop) (f : P MkAllah) (a : Allah) => match a as a0 return (P a0) with | MkAllah => f end : forall P : Allah -> Prop, P MkAllah -> forall a : Allah, P a
<@aweinstock> I figured as long as we were doing Allah and Induction jokes, I could define Allah as an inductive type (isomorphic to unit, because monotheism), and take the induction principle for it
<@aweinstock> you can recreate it (with colors, even) with `echo 'Inductive Allah := MkAllah. Print Allah_ind.' | coqtop`
About / Browse / Latest / Random / Queue / Prefs / Submit Quote / Search
14,775 quotes approved; 8,808 fermenting; karma: 189.4060