Subscribe to:
Post Comments (Atom)

Subscribe to:
Post Comments (Atom)

- Coq (11)
- Prolog (11)
- Haskell (4)
- Agda 2 (3)
- Lambda Calculus (3)
- Pattern Matching (3)
- Scheme (3)
- puzzle (3)
- stack (3)
- Dependent Types (2)
- Fin (2)
- GADT (2)
- HOAS (2)
- NbE (2)
- NoConfusion (2)
- Universes (2)
- beta (2)
- constraint logic programming (2)
- decidable equality (2)
- eta (2)
- ALGOL (1)
- Ackermann (1)
- BNF (1)
- Beta Function (1)
- C (1)
- CHR (1)
- CIC (1)
- CPS (1)
- Cantor (1)
- Cardinality (1)
- Chunks (1)
- Countable (1)
- Curry-Howard (1)
- DCG (1)
- Data.Dynamic (1)
- Delimeted Continuations (1)
- Deprogramming (1)
- Diagonalization (1)
- EBNF (1)
- EDSL (1)
- Embedded (1)
- Extraction (1)
- GADT nonsense (1)
- Generate and Test (1)
- Group (1)
- GĂ¶del (1)
- Hoare Logic (1)
- Huffman (1)
- Inducitive Families (1)
- Induction (1)
- Induction-Recursion (1)
- Infinity (1)
- Lisp (1)
- Magic Square (1)
- Monads (1)
- PTS (1)
- Parser combinators (1)
- Parsing (1)
- Permutation (1)
- Programming (1)
- Quest for Chunks (1)
- RLE (1)
- SET (1)
- SK (1)
- STLC (1)
- Semigroup (1)
- Shift/Reset (1)
- Specification (1)
- Strictly Positive Family (1)
- Subexpression elimination (1)
- Type Theory (1)
- Type inference (1)
- Variadic (1)
- Well Founded Relation (1)
- XOR (1)
- algebra (1)
- badger (1)
- compiler (1)
- constraint programming (1)
- correctness (1)
- correctness proof (1)
- counting (1)
- declarative (1)
- dependent destruct (1)
- dependently typed programming (1)
- differentation (1)
- foldl (1)
- foldr (1)
- heap (1)
- inhabitants (1)
- interpreter (1)
- irritated (1)
- java (1)
- lazy evaluation (1)
- lazy evalution (1)
- let-syntax (1)
- lights out (1)
- ltac (1)
- metatheory (1)
- model theory (1)
- mutation (1)
- pigeonhole principle (1)
- prime (1)
- prime seive (1)
- pure type systems (1)
- recursion (1)
- run length encoding (1)
- semantics (1)
- show instance (1)
- single constructor inductives (1)
- solving (1)
- syntax coloring (1)
- syntax-rules (1)
- tail call optimization (1)
- tauto (1)
- type checker (1)
- type checking (1)
- zeta (1)
- zipper (1)

## 5 comments:

I am confused and scared. Is this how people who believe in [ZFC/God] feel when they read [your post/that sign]?

What are you using to highlight coq code?

emacs proof-general htmlize-buffer

That's just a stupid statement. "There is probably..." That means the author is not sure and why would you not enjoy your life if there is a God. You should actually enjoy it more.

That's just a stupid statement. "There is probably..." That means the author is not sure and why would you not enjoy your life if there is a God. You should actually enjoy it more.

Post a Comment