#311618* (?/25) ⚐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` |