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

This quote has been fermenting for 2 months and has been voted on 6 times.
Based on preliminary voting, this quote has a 49.5% chance of being approved.

#311618* (?/6) ⚐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,786 quotes approved; 8,799 fermenting; karma: 189.3430