Alex pqnelson

As I understand it, Mizar uses the mml.lar file to read in the articles of the Mizar Mathematical Library in the specific order found in that file.

If you want to read the Mizar mathematical library's articles, it makes sense to study them in the order found in the mml.lar file.

I have linked to the article's abstracts found on Mizar's website.

DCAU Comic Recommendations

Introduction

The DC Universe website is sadly shutting down. They had, on the credits, a link to “associated comic book”. I thought I would compile the list of associated comics for each episode.

If someone wanted to start watching the DC Animated Universe but doesn’t

This is a growing list of project ideas which may be good for a budding programmer to try. The tasks vary in difficulty and length, but I try to make it language agnostic.

Unit testing is best done with BDD in mind.

BDD considers "stories" described in Gherkin (a DSL). Stories have the template:

As a (user)
In order to (achieve some end)
I want to (something to realize that end)

Then we create scenarios which would happen in this story.

	signature MONAD = sig
	type 'a m;
	val return : 'a -> 'a m;
	val bind : 'a m -> ('a -> 'b m) -> 'b m;
	end;

	signature IO_MONAD = sig
	include MONAD;
	val exec : 'a m -> 'a;
	val getStr : int -> TextIO.vector m;

	(*
	Some basic normal forms for propositional logic.

	So far, I have NNF, NENF, DNF, and CNF normalizations.

	This is mostly a translation of chapter 2 from John Harrison's _Handbook of Automated Reasoning and Practical Logic_.
	*)
	datatype 'a Formula = True
	\| False
	\| Atom of 'a

	-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
	import Data.List (delete, union)
	{- HLINT ignore "Eta reduce" -}

	-- File mnemonics:
	-- env = typing environment
	-- vid = variable identifier in Bind or Var
	-- br = binder variant (Lambda or Pi)
	-- xyzTyp = type of xyz
	-- body = body of Lambda or Pi abstraction

	import Data.Set

	type Letter = String

	data Term = TTau Integer Letter Relation
	\| TBox Integer Letter
	\| TVar Letter
	\| TSubst Term Letter Term
	\| TPair Term Term
	deriving (Show, Eq)

	#!/usr/bin/env python


	import fileinput
	from re import sub

	deletemode = False
	codemode = False
	asmmode = False
	breakmode = False

	<!-- https://fivethirtyeight.com/features/who-wants-to-be-a-senator-not-these-high-profile-democrats/ -->
	<p>Remember that in 2016, <a href="http://crystalball.centerforpolitics.org/crystalball/articles/senate-observations-placing-2018-in-the-context-of-upper-chamber-elections-since-1913/">for the</a> <a href="https://fivethirtyeight.com/features/there-were-no-purple-states-on-tuesday/">first time</a>,<a class="espn-footnote-link espn-footnote-item-expanded" data-footnote-id="1" href="#fn-1" data-footnote-content="<p>Or at least since popular Senate elections began <a href="https://constitutioncenter.org/interactive-constitution/amendments/amendment-xvii">after the ratification</a> of the 17th Amendment in 1913.</p>
	"><sup id="ss-1">x</sup></a><span class="espn-footnote-item espn-footnote-item-displayed espn-footnote-item-expanded"><span class="espn-footnote-item-inner"><span><p>Or at least since popular Senate elections began <a href="https://constitutioncenter.org/interactive-constitution/amendmen