pqnelson

The Make-a-HOL Process

• Prefatory Comments
• Pick a language
• The Make-A-HOL Process
  • Step 0: Tables
  • Step 1: Substitutions
  • Step 2: Types
  • Step 3: Terms
• Step 4: Matching

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.

pqnelson

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;

pqnelson

(*
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

pqnelson

-- 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

pqnelson

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

pqnelson

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)

pqnelson

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.

pqnelson

<!-- 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=&quot;https://constitutioncenter.org/interactive-constitution/amendments/amendment-xvii&quot;>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

pqnelson

#!/usr/bin/env python


import fileinput
from re import sub

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