It is a stock cheat in boxing for one to conceal something hard and heavy in one's glove. Classically done with a horseshoe.
A character employing this tactic in non-professional contexts is probably a Combat Pragmatist.
Interestingly, the point of a boxing glove is not to dampen the blow, it's to protect the hand. Hiding a horseshoe (or similarly hard things) in your boxing glove would be just as likely to damage your fingers as your opponent's face. This simply makes it an Acceptable Break from Reality.
Compare Power Fist; Power Fists may be used in straight fights as much as it is for cheating. Compare also Tricked-Out Gloves for gloves that are used for more than just punching. Handbag of Hurt and Sock It to Them also commonly go with a similar principle: something heavy is put inside the handbag/sock so it can pack hard hit.
Examples
- Used in a pillow fight in Mahou Sensei Negima!. Obviously, the rules call for pillows to be used, but Rules Lawyer Yue figures that she can use heavy books to hit her opponents if she's hitting the pillows (with them underneath). She is a lot more blatant about this when they realise she's hiding books in her pillows.
- In Rurouni Kenshin, Hannya, whose fighting style revolves around punching his enemies, hides iron knuckledusters in his otherwise normal looking gloves.
- In Spy vs. Spy, one spy used this trick to defeat the other — although, in the strip's usual Gambit Pileup fashion, the other spy spotted him doing it and came into the ring wearing a mask of his own face over an iron helmet.
- Played for Laughs in one issue of Little Archie. Little Jughead gives Little Archie a pair of lead weights while they're training for a boxing match; he instantly refuses, saying "That's cheating." Jughead informs him that the weights are only for training purposes; when they take the weights out for the real fight, his punches will be harder. Mr. Weatherbee brings some of his colleagues to watch the pair train, and Archie's glove slips off and hits Weatherbee in his Glass Jaw. The other teachers comment "Wow, knocked out by an empty glove!"
- Happens in the Steampunk Halloween 2012 comic from Antarctic Press. A boxer fighting Dr Frankensteam's creation slips a horseshoe into his glove. However, the horseshoe shatters when he punches the monster.
- Played for Laughs in Cattivik when he's forced in a match against a much larger wrestler and dons massive gloves filled with iron scraps. When the referee points out that they're against the rules, he retorts by pointing out how his opponent gets to keep a whole living anaconda with him.
- At one point Spider-Girl Anya Corazon is given a makeover by the heroes in the Avengers. One of their upgrades are leather gloves with metal dust in the knuckles.
- Parodied by the IDW Popeye comics. In issue #4, Popeye takes a horrible beating in a match with a masked boxer. Turns out the opponent has horseshoes in his gloves... and what's more, he's an actual horse!
- In Eight Count, Slade Wilson lost his eye in a boxing match years before the main story when an opponent loaded his gloves with metal.
- Ancillary materials to Batman Begins explain that Bruce packed the Batsuit's gloves with lead shot.
- An early example can be found in the 1915 movie The Champion, where Charlie Chaplin finds a "good luck" horseshoe just as he passes a training camp advertising for a boxing partner "who can take a beating." After watching others lose badly, Charlie decides to enhance his chances of survival by sneaking the horseshoe into his right glove. Of course, he wins the fight.
- Subverted in Chaplin's later film City Lights, which has a similar plot of the hero volunteering for a box fight to raise money. In the locker room he finds a horseshoe which he fiddles with but eventually dismisses and goes to fight without. We can only assume that Chaplin figured that people would have seen the previous horseshoe scene in The Champion and expected him to try the same trick again. This time he fools them by tossing it away.
- Eamann, a local bully, hides stones in his hand wraps for his climactic fight against Frances in Float Like A Butterfly.
- In The Red Vixen Adventures Alinadar wears Fingerless Gloves with lead weights, among several other easily concealed weapons.
- Discworld. In Night Watch, Sam Vimes lays out Ronald Rust with this trick, then turns to his men, rubs his knuckles and says
''Important lesson, lads. It hurts, no matter what you do.
- In By The Great Horn Spoon, which is set during the 1840s California Gold Rush, the butler Praiseworthy hides gold dust in his gloves to keep it from being found. Later their coach is robbed, and Praiseworthy socks one of the robbers several feet into the air with his gold-weighted gloves. As such he gets rumored around town to be an incredible fistfighter, and so starts studying boxing to keep up his reputation for the real fights.
- Brought up in Welkin Weasels, when Prince Poynt suggests cheating at a boxing match by weighting his favoured boxer's gloves. It doesn't work, as it's then explained to him that it's a bare-knuckle boxing match.
- The "Fight Night" episode of CSI centered on a boxing match. The winner of the match was found to have injected mercury into his glove.
- In the "Collateral Damage" episode of Blue Bloods a bunch of executives engage in boxing Fight Club. When one of them dies after a match, the detectives find that the winner's gloves have been doctored to make them heavier.
- In the "Old Mrs. Old" episode of Malcolm in the Middle, Dewey carries a purse (or man-handbag) to school and is bullied by other kids on the way home for doing so. But then he swings it at one of the kids, and whap!—turns out he put a brick inside it.
- A variant: The episode "Requiem for a Lightweight" from M*A*S*H has Trapper agree to fight General Barker's goon to win back a pretty nurse. Knowing he'd be pummeled to jelly otherwise, Trapper allows Hawkeye to soak his boxing gloves in ether. By keeping his glove near his opponent's nose, Trapper exposes him to enough ether fumes to pass out in the ring, thus winning the match.
- Agents of S.H.I.E.L.D. has a Villain of the Week who plays with this trope. Carl Creel note could change parts or all of his body into anything he touched. Before getting recruited by HYDRA, he was a boxer and would hide steel hands under his gloves.
- In the Miss Fisher's Murder Mysteries episode "Deadweight" Weighted Gloves are used against a young boxer in a local boxing ring until Constable Hugh Collins steps in and tells them to ditch them.
- The Smallville episode "Jinx" reverses this as Clark plans to hide a piece of kryptonite in his football gloves to try to weaken himself so he can compete on a level footing. It doesn't work.
- The Doctor Blake Mysteries: In "A Lethal Combination", Charlie's brother Ray has his hand wraps coated in plaster of Paris before a boxing match. As the match progresses, the plaster absorbs sweat and hardens, allowing him to deliver much more solid blows.
- The Westerner: Denny Lipp, the bad guy in "Jeff", does the bare knuckle equivalent of this trope: soaking his fists in brine before a fight to harden his punches.
- The Iron Sheik had a loaded boot. When he set his opponent up for the finisher, he'd shake his boot, causing all the lead pellets (or whatever was supposed to be in there) to collect at the tip of his boot, so a kick would knock his opponent unconscious.
- There's a minor character in Skyrim who boasts about winning a brawl by using a horseshoe as a knuckle-duster. Fittingly, his name is Irnskar Iron-Hand.
- In Fallout 2, you can make a name for yourself as a boxer in New Reno. During the boxing matches, you are stripped of all equipment and given a pair of boxing gloves to fight with, and any other attack will disqualify the PC. The boxing gloves deal very little damage, and the PC needs either good critical hits or dedicated damage perks to win. However, in the same city, you can find a pair of boxing gloves with plates slipped into the knuckles, allowing all but the last fight to be won by dealing hit point damage (it is possible for a character to be too weak in combat to do even that, but most such characters are disallowed from the boxing ring anyway).
- A variation in The Legend of Zelda: Twilight Princess: in order to get into the Goron Mines, you need to defeat their elder in a sumo match. The Gorons are twice Link's height and made of stone, so naturally he gets sent flying in a second. Link asks the only human ever to defeat a Goron in sumo wrestling, who reveals he used a little secret: massive weighted boots that allowed him to withstand the Goron's charge. The Gorons are very much against cheating, but they never notice you putting the boots on.
- Aran Ryan in the Wii version of Punch-Out!! is shown stuffing horseshoes in his gloves in his Contender intro, as pictured above. As thoroughly unsubtle as it is, that's not even his most glaring cheating manoeuvre: that honour has to go to how he expands on the idea in Title Defence. One of his old gloves wears out, so he takes it, attaches it to a long rope, stuffs even more horseshoes into it, and wields it as a heavy whip weapon.
- In Use Sword on Monster Hilda wears sap gloves, not really legal but useful for taking someone out without killing them. Especially seeing how as a "sword-swinger" the magic makes her fight on autopilot until her enemy is no longer a threat.
- Merrie Melodies
- There is a cartoon where, after a boxer lands an especially telling punch, the referee stops the bout and checks the boxer's glove. Upon removing and shaking the glove, out drops a horseshoe... then three more horseshoes... then a confused-looking horse.
- In "Hare Trimming", Bugs pretends to be a French gentlemen rival to Yosemite Sam for the love of a rich widow. Sam gives Bugs "a taste of leather" and Bugs responds in kind... but not before putting a brick inside the glove. After hitting Sam, he shakes out the pulverized remains.
- In Porky Pig's Feat, Daffy, having lost the money to pay his and Porky's hotel bill in a craps game, insults the hotel manager after refusing to pay. The manager slaps Daffy with his glove and challenges him to a duel ("You have insulted me! We meet on the field of honor! My Card"). Daffy then slips a horseshoe into a glove and imitates the challenge ("You have insult me!  When Bugs removes his, two horseshoes fall out of each one.
- The 1950 Friz Freleng cartoon "Stooge For A Mouse" has a hungry mouse load horseshoes into a boxing glove, then tie the glove onto Sylvester's hand while the cat naps. The mouse then uses a magnet below the floorboards to compel Sylvester to fly at a bulldog fist-first. Once the cat and dog have demolished each other, the mouse has a clear shot at the Cartoon Cheese.
- A Handbag of Hurt variation in "Boston Quackie"; Marie beans the Man in the Green Hat with her purse, then shows Quackie that she carries an anvil in it.
- The Simpsons. In "The Homer They Fall" episode, Homer sees that Moe has a boxing glove with barbed wire on it which Moe refers to as "The Stinger". Moe says "yeah, they don't let you use that no more."
- In the Donald Duck cartoon "Canvas Back Duck", Donald's nephews put scraps of metal in his glove, but it only makes the glove too heavy to lift. His hand slips off and his fist accidentally hits the other fighter in the jaw. Fortunately, the opponent had a "glass jaw" and is out like a light.
- On the Goofy cartoon "The Art of Self-Defense", two 18th Century dandies slap each other with gloves. During a break in the action, one of them sneaks his snuff box into his glove.
- Tex Avery's Lonesome Lenny has a gag where the titular dog punches Screwy Squirrel with a hard boxing glove. Screwy then empties out four horseshoes... plus the horse.
- Legend of Korra. In probending, waterbenders are the only ones allowed to use headshots due to the Soft Water trope. One of the ways the Wolfbats cheat is by adding rocks into their water missiles, which does more damage.
- Tiny Toon Adventures also used the "horseshoes-and-horse-in-the-glove" variant of the gag in "Citizen Max".
- Sap gloves are leather or vinyl gloves with weights sewn into the knuckles. Their primary intention is to protect the wearer from injury, while the metal powder or shot adds mass and thus kinetic energy to the punch. Properly executed, they can be used to punch through glass and concrete.
- The annual pillow fight at the United States Military Academy was a long-standing tradition. But in 2015, some of the more gung-ho cadets over-did it by adding unauthorised fillings to their pillowcases, up to and including metal footlocker boxes. Apparently thirty cadets were hospitalised and West Point officials investigated the event. See here.
- The tragic case of Billy Collins v. Luis Resto. Before the match, Resto's trainer soaked Resto's hand wraps in plaster of Paris and removed the padding from his gloves, resulting in his punches hitting far harder than they would have otherwise. After an investigation, Resto was banned from boxing and spent several years in prison.


Multer is a node.js middleware for handling
multipart/form-data
, which is primarily used for uploading
files. It is written on top of
busboy for maximum
efficiency.
NOTE: Multer will not process any form which is not
multipart (multipart/form-data
).
This README is also available in other languages:
Multer adds a body
object and a file
or
files
object to the request
object. The
body
object contains the values of the text fields of the
form, the file
or files
object contains the
files uploaded via the form.
Basic usage example:
Don’t forget the enctype="multipart/form-data"
in your form.
<form action="/profile" method="post" enctype="multipart/form-data">
<input type="file" name="avatar" />
</form>
var express = require('express')
var multer = require('multer')
var upload = multer({ dest: 'uploads/' })
var app = express()
app.post('/profile', upload.single('avatar'), function (req, res, next) {
// req.file is the `avatar` file
// req.body will hold the text fields, if there were any
})
app.post('/photos/upload', upload.array('photos', 12), function (req, res, next) {
// req.files is array of `photos` files
// req.body will contain the text fields, if there were any
})
var cpUpload = upload.fields([{ name: 'avatar', maxCount: 1 }, { name: 'gallery', maxCount: 8 }])
app.post('/cool-profile', cpUpload, function (req, res, next) {
// req.files is an object (String -> Array) where fieldname is the key, and the value is array of files
//
// e.g.
// req.files['avatar'][0] -> File
// req.files['gallery'] -> Array
//
// req.body will contain the text fields, if there were any
})
In case you need to handle a text-only multipart form, you should use the
.none()
method:
var express = require('express')
var app = express()
var multer = require('multer')
var upload = multer()
app.post('/profile', upload.none(), function (req, res, next) {
// req.body contains the text fields
})
Here’s an example on how multer is used an HTML form. Take special note of
the enctype="multipart/form-data"
and
name="uploaded_file"
fields:
<form action="/stats" enctype="multipart/form-data" method="post">
<div class="form-group">
<input type="file" class="form-control-file" name="uploaded_file">
<input type="text" class="form-control" placeholder="Number of speakers" name="nspeakers">
<input type="submit" value="Get me the stats!" class="btn btn-default">
</div>
</form>
Then in your javascript file you would add these lines to access both the
file and the body. It is important that you use the
name
field value from the form in your upload function. This
tells multer which field on the request it should look for the files in.
If these fields aren’t the same in the HTML form and on your server, your
upload will fail:
var multer = require('multer')
var upload = multer({ dest: './public/data/uploads/' })
app.post('/stats', upload.single('uploaded_file'), function (req, res) {
// req.file is the name of your file in the form above, here 'uploaded_file'
// req.body will hold the text fields, if there were any
console.log(req.file, req.body)
});
Each file contains the following information:
| Key | Description | Note |
|---|---|---|
fieldname |
Field name specified in the form | |
originalname |
Name of the file on the user’s computer | |
encoding |
Encoding type of the file | |
mimetype |
Mime type of the file | |
size |
Size of the file in bytes | |
destination |
The folder to which the file has been saved | DiskStorage |
filename |
The name of the file within the destination |
DiskStorage |
path |
The full path to the uploaded file | DiskStorage |
buffer |
A Buffer of the entire file |
MemoryStorage |
multer(opts)
Multer accepts an options object, the most basic of which is the
dest
property, which tells Multer where to upload the files.
In case you omit the options object, the files will be kept in memory and
never written to disk.
By default, Multer will rename the files so as to avoid naming conflicts. The renaming function can be customized according to your needs.
The following are the options that can be passed to Multer.
| Key | Description |
|---|---|
dest or storage |
Where to store the files |
fileFilter |
Function to control which files are accepted |
limits |
Limits of the uploaded data |
preservePath |
Keep the full path of files instead of just the base name |
In an average web app, only dest
might be required, and
configured as shown in the following example.
If you want more control over your uploads, you’ll want to use the
storage
option instead of dest
. Multer ships
with storage engines DiskStorage
and
MemoryStorage
; More engines are available from third parties.
.single(fieldname)
Accept a single file with the name fieldname
. The single file
will be stored in req.file
.
.array(fieldname[, maxCount])
Accept an array of files, all with the name fieldname
.
Optionally error out if more than maxCount
files are
uploaded. The array of files will be stored in req.files
.
.fields(fields)
Accept a mix of files, specified by fields
. An object with
arrays of files will be stored in req.files
.
fields
should be an array of objects with
name
and optionally a maxCount
. Example:
.none()
Accept only text fields. If any file upload is made, error with code “LIMIT_UNEXPECTED_FILE” will be issued.
.any()
Accepts all files that comes over the wire. An array of files will be
stored in req.files
.
WARNING: Make sure that you always handle the files that a user uploads. Never add multer as a global middleware since a malicious user could upload files to a route that you didn’t anticipate. Only use this function on routes where you are handling the uploaded files.
storage
DiskStorage
The disk storage engine gives you full control on storing files to disk.
var storage = multer.diskStorage({
destination: function (req, file, cb) {
cb(null, '/tmp/my-uploads')
},
filename: function (req, file, cb) {
const uniqueSuffix = Date.now() + '-' + Math.round(Math.random() * 1E9)
cb(null, file.fieldname + '-' + uniqueSuffix)
}
})
var upload = multer({ storage: storage })
There are two options available, destination
and
filename
. They are both functions that determine where the
file should be stored.
destination
is used to determine within which folder the
uploaded files should be stored. This can also be given as a
string
(e.g. '/tmp/uploads'
). If no
destination
is given, the operating system’s default
directory for temporary files is used.
Note: You are responsible for creating the directory when
providing destination
as a function. When passing a string,
multer will make sure that the directory is created for you.
filename
is used to determine what the file should be named
inside the folder. If no filename
is given, each file will be
given a random name that doesn’t include any file extension.
Note: Multer will not append any file extension for you, your function should return a filename complete with an file extension.
Each function gets passed both the request (req
) and some
information about the file (file
) to aid with the decision.
Note that req.body
might not have been fully populated yet.
It depends on the order that the client transmits fields and files to the
server.
For understanding the calling convention used in the callback (needing to pass null as the first param), refer to Node.js error handling
MemoryStorage
The memory storage engine stores the files in memory as
Buffer
objects. It doesn’t have any options.
When using memory storage, the file info will contain a field called
buffer
that contains the entire file.
WARNING: Uploading very large files, or relatively small files in large numbers very quickly, can cause your application to run out of memory when memory storage is used.
limits
An object specifying the size limits of the following optional properties. Multer passes this object into busboy directly, and the details of the properties can be found on busboy’s page.
The following integer values are available:
| Key | Description | Default |
|---|---|---|
fieldNameSize |
Max field name size | 100 bytes |
fieldSize |
Max field value size (in bytes) | 1MB |
fields |
Max number of non-file fields | Infinity |
fileSize |
For multipart forms, the max file size (in bytes) | Infinity |
files |
For multipart forms, the max number of file fields | Infinity |
parts |
For multipart forms, the max number of parts (fields + files) | Infinity |
headerPairs |
For multipart forms, the max number of header key=>value pairs to parse | 2000 |
Specifying the limits can help protect your site against denial of service (DoS) attacks.
fileFilter
Set this to a function to control which files should be uploaded and which should be skipped. The function should look like this:
function fileFilter (req, file, cb) {
// The function should call `cb` with a boolean
// to indicate if the file should be accepted
// To reject this file pass `false`, like so:
cb(null, false)
// To accept the file pass `true`, like so:
cb(null, true)
// You can always pass an error if something goes wrong:
cb(new Error('I don\'t have a clue!'))
}
When encountering an error, Multer will delegate the error to Express. You can display a nice error page using the standard express way.
If you want to catch errors specifically from Multer, you can call the
middleware function by yourself. Also, if you want to catch only
the Multer errors, you can use the MulterError
class that is attached to the
multer
object itself (e.g. err instanceof multer.MulterError
).
var multer = require('multer')
var upload = multer().single('avatar')
app.post('/profile', function (req, res) {
upload(req, res, function (err) {
if (err instanceof multer.MulterError) {
// A Multer error occurred when uploading.
} else if (err) {
// An unknown error occurred when uploading.
}
// Everything went fine.
})
})
For information on how to build your own storage engine, see Multer Storage Engine.


There is no one who became rich because he broke a holiday, no one became fat because he broke a fast.
~ Ethiopian proverb


As a member of the European Union, EU regulations apply. Reporting in or out is not normally enforced but occasionally an official (Police) will check that Passports are in order and say that they should be stamped.
It is advisable that crew members arriving by plane request their passports are stamped at the airport.
Yachts arriving from Greenland, Norway or EU countries, with nothing to declare, do not have to report to Customs on arrival. Others should proceed to a Port of Entry and report to Customs.
It should be noted that duty-free allowances are very small and amounts over this are declarable. Customs do check yachts, so if in doubt it is advisable to report to Customs.
Immigration must be cleared on arrival and departure. A comprehensive list of all safety equipment on board may be requested by Customs.
See comment about harbour masters at bottom of page.
Last updated August 2015.
Denmark is a member of the Schengen Agreement Area. See Noonsite' Schengen page for more details on the immigration rules and a link to the Schengen Visa application form.
The current requirements for visas for Denmark and The Faroe Islands can be found at www.nyidanmark.dk
Last updated September 2016.
Firearms must be declared.
The importation of milk, dairy products and eggs as well as perishable meat or meat products is only permitted with a special licence.
If a yacht has a large amount of dutiable goods in excess of the allowed limits, the stores must be placed under Customs seal and re-exported aboard the yacht. A deposit must be paid, which will be refunded after departure from Danish waters by returning the certificate supplied by the Danish customs office, after it has been stamped by customs on arrival in the next country confirming that the same amount of goods are on board.
EU regulations apply concerning temporary importation of yachts. See Noonsite's EU VAT page for more information.
Last updated August 2015.
"Health Advice for Travellers" produced by the Department of Health can be obtained for UK travellers by phoning 0800 555777
Yachts must carry their original registration document, insurance policy (although insurance is not mandatory in Denmark), and ship's radio licence. One member of the crew must have a radio operator’s certificate of competence. An inventory of the safety equipment on board. Other requirements are as for the visiting boats' flag state.
For EU boats, proof of VAT status is also required.
All crew should have valid passports.
Prohibited areas are military firing areas, information on which is contained on Danish charts and in the Danish Notices to Mariners. Also marked on Danish charts as restricted are several small uninhabited islands, which are protected areas for seabirds and other wildlife and should not be landed on between 1 April and 1 June. On some of these islands there are signs forbidding landing.
Navigation: Shipping traffic between the North Sea and the Baltic is heavy and vessels must use the correct lane in traffic separation zones. These are in operation in the northern part of the Sound between Elsinore and Hälsingborg in Sweden, at the Great Belt between Korsør and Sprogoe by Hatter Barn and the Baltic Sea south of Gedser. In Danish waters the Transit Route for very large vessels runs from the Skaw to the Moen SE light vessel north-east of Gedser. In some areas larger ships on the Transit Route are confined by depths to Deep Water Routes; these can be found in the Great Belt east of Samsoe, along the east coast of Langeland, and north-east of Gedser. Yachts should avoid the Transit and Deep Water Routes as the depth conditions do not allow large vessels much room to manoeuvre. Attention should also be paid to port entry regulations and signs.
Fishing: Foreign visitors may only use simple hand gear for fishing. Harpoons, traps and nets are forbidden. Permission should be obtained from the owners of the fishing rights before fishing in rivers or estuaries.
Holding Tanks - whilst Denmark has implemented the recommendaions (with exceptions as listed below), the Danish Sailing Association advise that foreign visitors will not be compelled to have holding tanks. Furthermore, not all Danish harbours have to equipment to pump out tanks. Exceptions - Boats built before 1st January 1980 do not have to have holding tanks. Boats built after 1st January 1980 but before 1st January 2000 and which are either less than 10.5m LOA or have a maximum beam of less than 2.8m do not have to have a holding tank. Boats outside the above exemptions, including all boats built after 1st January 2000, must have a holding tank than can be emptied through a deck fitting. Boats which are required to have holding tanks must empty them either in official places in harbours or outside a 12NM limited from the coast. Boats not required to have tanks may discharge toilets outside a 1NM limited from the coast.
It is expected that the yacht's ensign be taken down by 21:00 (or sunset if earlier) and raised again at 08:00 (or sunrise if later).
In harbour, it is expected that crews should be quiet after 22:00.
Denmark accepts animals covered by PETS (Pets Travel Scheme) with current Passport, Health Certificate and Rabies Vaccination Certificate and have been microchipped and blood tested prior to import.
Denmark requires certificates to be bilingual.
Go to www.pettravelstore for forms.


Note that: browser support for different color spaces is somewhat patchy. Browsers that do support the newer color spacess in CSS may not support them in <canvas> elements.
Chrome issue: while Chrome supports LAB/LCH and OKLAB/OKLCH color spaces, it does not parse these colors correctly when the non-L values are given in % format.
For browsers that do not currently support a given color space (eg: Firefox), SC will calculate the required color space color (for all permitted formatting values) and render the color on the canvas using the sRGB color space.
Touch test: not required
Test if color strings work for CSS in this browser:


Layouts are standalone http services which on run time compose one or multiple Podlets (page fragments) into full webpages. This is a Layout, which will include the Podlet in our example, built with Express.js.
const express = require('express');
const Layout = require('@podium/layout');
const layout = new Layout({
name: 'myLayout',
pathname: '/'
});
const podlet = layout.client.register({
name: 'myPodlet',
uri: 'http://localhost:7100/manifest.json'
});
const app = express();
app.use(layout.middleware());
app.get('/', async (req, res) => {
const content = await podlet.fetch();
res.send(`
${content}
`);
});
app.listen(7000);
Start the Layout and it will be accessable on http://localhost:7000/


ListsData Structures in Coq
(* $Date: 2012-01-15 17:51:17 -0500 (Sun, 15 Jan 2012) $ *)
The next line imports all of our definitions from the
previous chapter.
For it to work, you need to use coqc to compile Basics.v
into Basics.vo. (This is like making a .class file from a .java
file, or a .o file from a .c file.)
Here are two ways to compile your code:
In this file, we again use the Module feature to wrap all of the
definitions for pairs and lists of numbers in a module so that,
later, we can reuse the same names for improved (generic) versions
of the same operations.
- CoqIDE:
Open Basics.v. In the "Compile" menu, click on "Compile Buffer".
- Command line:
Run coqc Basics.v
Pairs of Numbers
This declaration can be read: "There is just one way to
construct a pair of numbers: by applying the constructor pair to
two arguments of type nat."
Here are some simple function definitions illustrating pattern
matching on two-argument constructors:
Definition fst (p : natprod) : nat :=
match p with
| pair x y => x
end.
Definition snd (p : natprod) : nat :=
match p with
| pair x y => y
end.
Since pairs are used quite a bit, it is nice to be able to
write them with the standard mathematical notation (x,y) instead
of pair x y. We can tell Coq to allow this with a Notation
declaration.
The new notation can be used both in expressions and in
pattern matches (indeed, we've seen it already in the previous
chapter — this notation is provided as part of the standard
library):
Eval simpl in (fst (3,4)).
Definition fst' (p : natprod) : nat :=
match p with
| (x,y) => x
end.
Definition snd' (p : natprod) : nat :=
match p with
| (x,y) => y
end.
Definition swap_pair (p : natprod) : natprod :=
match p with
| (x,y) => (y,x)
end.
Let's try and prove a few simple facts about pairs. If we
state the lemmas in a particular (and slightly peculiar) way, we
can prove them with just reflexivity (and its built-in
simplification):
Theorem surjective_pairing' : ∀ (n m : nat),
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity. Qed.
But reflexivity is not enough if we state the lemma in a more
natural way:
Theorem surjective_pairing_stuck : ∀ (p : natprod),
p = (fst p, snd p).
Proof.
simpl. (* Doesn't reduce anything! *)
Admitted.
We have to expose the structure of p so that simpl can
perform the pattern match in fst and snd. We can do this with
destruct.
Notice that, unlike for nats, destruct doesn't generate an
extra subgoal here. That's because natprods can only be
constructed in one way.
Theorem surjective_pairing : ∀ (p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as (n,m). simpl. reflexivity. Qed.
Notice that Coq allows us to use the notation we introduced
for pairs in the "as..." pattern telling it what variables to
bind.
Exercise: 1 star (snd_fst_is_swap)
Theorem snd_fst_is_swap : ∀ (p : natprod),
(snd p, fst p) = swap_pair p.
Proof.
(* FILL IN HERE *) Admitted.
(snd p, fst p) = swap_pair p.
Proof.
(* FILL IN HERE *) Admitted.
Theorem fst_swap_is_snd : ∀ (p : natprod),
fst (swap_pair p) = snd p.
Proof.
(* FILL IN HERE *) Admitted.
fst (swap_pair p) = snd p.
Proof.
(* FILL IN HERE *) Admitted.
☐
Generalizing the definition of pairs a little, we can
describe the type of lists of numbers like this: "A list is
either the empty list or else a pair of a number and another
list."
Lists of Numbers
For example, here is a three-element list:
As with pairs, it is more convenient to write lists in
familiar programming notation. The following two declarations
allow us to use :: as an infix cons operator and square
brackets as an "outfix" notation for constructing lists.
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
It is not necessary to fully understand these declarations,
but in case you are interested, here is roughly what's going on.
The right associativity annotation tells Coq how to parenthesize
expressions involving several uses of :: so that, for example,
the next three declarations mean exactly the same thing:
Definition l_123' := 1 :: (2 :: (3 :: nil)).
Definition l_123'' := 1 :: 2 :: 3 :: nil.
Definition l_123''' := [1,2,3].
The at level 60 part tells Coq how to parenthesize
expressions that involve both :: and some other infix operator.
For example, since we defined + as infix notation for the plus
function at level 50,
(By the way, it's worth noting in passing that expressions like "1
+ 2 :: [3]" can be a little confusing when you read them in a .v
file. The inner brackets, around 3, indicate a list, but the outer
brackets are there to instruct the "coqdoc" tool that the bracketed
part should be displayed as Coq code rather than running text.
These brackets don't appear in the generated HTML.)
The second and third Notation declarations above introduce the
standard square-bracket notation for lists; the right-hand side of
the third one illustrates Coq's syntax for declaring n-ary
notations and translating them to nested sequences of binary
constructors.
A number of functions are useful for manipulating lists.
For example, the repeat function takes a number n and a
count and returns a list of length count where every element
is n.
Notation "x + y" := (plus x y)
(at level 50, left associativity).
The + operator will bind tighter than ::, so 1 + 2 :: [3]
will be parsed, as we'd expect, as (1 + 2) :: [3] rather than 1
+ (2 :: [3]).
(at level 50, left associativity).
Fixpoint repeat (n count : nat) : natlist :=
match count with
| O => nil
| S count' => n :: (repeat n count')
end.
The length function calculates the length of a list.
The app ("append") function concatenates two lists.
Fixpoint app (l1 l2 : natlist) : natlist :=
match l1 with
| nil => l2
| h :: t => h :: (app t l2)
end.
Actually, app will be used a lot in some parts of what
follows, so it is convenient to have an infix operator for it.
Notation "x ++ y" := (app x y)
(right associativity, at level 60).
Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4,5] = [4,5].
Proof. reflexivity. Qed.
Example test_app3: [1,2,3] ++ nil = [1,2,3].
Proof. reflexivity. Qed.
Here are two more small examples of programming with lists.
The hd function returns the first element (the "head") of the
list, while tail returns everything but the first
element. Of course, the empty list has no first element, so we
must pass a default value to be returned in that case.
Definition hd (default:nat) (l:natlist) : nat :=
match l with
| nil => default
| h :: t => h
end.
Definition tail (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => t
end.
Example test_hd1: hd 0 [1,2,3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tail: tail [1,2,3] = [2,3].
Proof. reflexivity. Qed.
Exercise: 2 stars, recommended (list_funs)
Complete the definitions of nonzeros, oddmembers and countoddmembers below.Fixpoint nonzeros (l:natlist) : natlist :=
(* FILL IN HERE *) admit.
Example test_nonzeros: nonzeros [0,1,0,2,3,0,0] = [1,2,3].
(* FILL IN HERE *) Admitted.
Fixpoint oddmembers (l:natlist) : natlist :=
(* FILL IN HERE *) admit.
Example test_oddmembers: oddmembers [0,1,0,2,3,0,0] = [1,3].
(* FILL IN HERE *) Admitted.
Fixpoint countoddmembers (l:natlist) : nat :=
(* FILL IN HERE *) admit.
Example test_countoddmembers1: countoddmembers [1,0,3,1,4,5] = 4.
(* FILL IN HERE *) Admitted.
Example test_countoddmembers2: countoddmembers [0,2,4] = 0.
(* FILL IN HERE *) Admitted.
Example test_countoddmembers3: countoddmembers nil = 0.
(* FILL IN HERE *) Admitted.
☐
Note: one natural way of writing alternate will fail to satisfy
Coq's requirement that all Fixpoint definitions be "obviously
terminating." If you find yourself in this rut, look for a
slightly more verbose solution that considers elements of both
lists at the same time.
Exercise: 2 stars (alternate)
Complete the definition of alternate, which "zips up" two lists into one, alternating between elements taken from the first list and elements from the second. See the tests below for more specific examples.Fixpoint alternate (l1 l2 : natlist) : natlist :=
(* FILL IN HERE *) admit.
Example test_alternate1: alternate [1,2,3] [4,5,6] = [1,4,2,5,3,6].
(* FILL IN HERE *) Admitted.
Example test_alternate2: alternate [1] [4,5,6] = [1,4,5,6].
(* FILL IN HERE *) Admitted.
Example test_alternate3: alternate [1,2,3] [4] = [1,4,2,3].
(* FILL IN HERE *) Admitted.
Example test_alternate4: alternate [] [20,30] = [20,30].
(* FILL IN HERE *) Admitted.
☐
A bag (or multiset) is like a set, but each element can appear
multiple times instead of just once. One reasonable
implementation of bags is to represent a bag of numbers as a
list.
Bags via Lists
Exercise: 3 stars (bag_functions)
Complete the following definitions for the functions count, sum, add, and member for bags.
All these proofs can be done just by reflexivity.
Example test_count1: count 1 [1,2,3,1,4,1] = 3.
(* FILL IN HERE *) Admitted.
Example test_count2: count 6 [1,2,3,1,4,1] = 0.
(* FILL IN HERE *) Admitted.
Multiset sum is similar to set union: sum a b contains
all the elements of a and of b. (Mathematicians usually
define union on multisets a little bit differently, which
is why we don't use that name for this operation.)
For sum we're giving you a header that does not give explicit
names to the arguments. Moreover, it uses the keyword
Definition instead of Fixpoint, so even if you had names for
the arguments, you wouldn't be able to process them recursively.
The point of stating the question this way is to encourage you to
think about whether sum can be implemented in another way —
perhaps by using functions that have already been defined.
Definition sum : bag → bag → bag :=
(* FILL IN HERE *) admit.
Example test_sum1: count 1 (sum [1,2,3] [1,4,1]) = 3.
(* FILL IN HERE *) Admitted.
Definition add (v:nat) (s:bag) : bag :=
(* FILL IN HERE *) admit.
Example test_add1: count 1 (add 1 [1,4,1]) = 3.
(* FILL IN HERE *) Admitted.
Example test_add2: count 5 (add 1 [1,4,1]) = 0.
(* FILL IN HERE *) Admitted.
Definition member (v:nat) (s:bag) : bool :=
(* FILL IN HERE *) admit.
Example test_member1: member 1 [1,4,1] = true.
(* FILL IN HERE *) Admitted.
Example test_member2: member 2 [1,4,1] = false.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (bag_more_functions)
Here are some more bag functions for you to practice with.Fixpoint remove_one (v:nat) (s:bag) : bag :=
(* When remove_one is applied to a bag without the number to remove,
it should return the same bag unchanged. *)
(* FILL IN HERE *) admit.
Example test_remove_one1: count 5 (remove_one 5 [2,1,5,4,1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_one2: count 5 (remove_one 5 [2,1,4,1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_one3: count 4 (remove_one 5 [2,1,4,5,1,4]) = 2.
(* FILL IN HERE *) Admitted.
Example test_remove_one4:
count 5 (remove_one 5 [2,1,5,4,5,1,4]) = 1.
(* FILL IN HERE *) Admitted.
Fixpoint remove_all (v:nat) (s:bag) : bag :=
(* FILL IN HERE *) admit.
Example test_remove_all1: count 5 (remove_all 5 [2,1,5,4,1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_all2: count 5 (remove_all 5 [2,1,4,1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_all3: count 4 (remove_all 5 [2,1,4,5,1,4]) = 2.
(* FILL IN HERE *) Admitted.
Example test_remove_all4: count 5 (remove_all 5 [2,1,5,4,5,1,4,5,1,4]) = 0.
(* FILL IN HERE *) Admitted.
Fixpoint subset (s1:bag) (s2:bag) : bool :=
(* FILL IN HERE *) admit.
Example test_subset1: subset [1,2] [2,1,4,1] = true.
(* FILL IN HERE *) Admitted.
Example test_subset2: subset [1,2,2] [2,1,4,1] = false.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
☐
Just as with numbers, simple facts about list-processing
functions can sometimes be proved entirely by simplification. For
example, the simplification performed by reflexivity is enough
for this theorem...
Exercise: 3 stars, recommended (bag_theorem)
Write down an interesting theorem about bags involving the functions count and add, and prove it. Note that, since this problem is somewhat open-ended, it's possible that you may come up with a theorem which is true, but whose proof requires techniques you haven't learned yet. Feel free to ask for help if you get stuck!☐
Reasoning About Lists
... because the [] is substituted into the match position
in the definition of app, allowing the match itself to be
simplified.
Also, as with numbers, it is sometimes helpful to perform case
analysis on the possible shapes (empty or non-empty) of an unknown
list.
Theorem tl_length_pred : ∀ l:natlist,
pred (length l) = length (tail l).
Proof.
intros l. destruct l as [| n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
reflexivity. Qed.
Here, the nil case works because we've chosen to define
tl nil = nil. Notice that the as annotation on the destruct
tactic here introduces two names, n and l', corresponding to
the fact that the cons constructor for lists takes two
arguments (the head and tail of the list it is constructing).
Usually, though, interesting theorems about lists require
induction for their proofs.
Simply reading example proofs will not get you very far! It is
very important to work through the details of each one, using Coq
and thinking about what each step of the proof achieves.
Otherwise it is more or less guaranteed that the exercises will
make no sense.
Proofs by induction over datatypes like natlist are
perhaps a little less familiar than standard natural number
induction, but the basic idea is equally simple. Each Inductive
declaration defines a set of data values that can be built up from
the declared constructors: a boolean can be either true or
false; a number can be either O or S applied to a number; a
list can be either nil or cons applied to a number and a list.
Moreover, applications of the declared constructors to one another
are the only possible shapes that elements of an inductively
defined set can have, and this fact directly gives rise to a way
of reasoning about inductively defined sets: a number is either
O or else it is S applied to some smaller number; a list is
either nil or else it is cons applied to some number and some
smaller list; etc. So, if we have in mind some proposition P
that mentions a list l and we want to argue that P holds for
all lists, we can reason as follows:
Since larger lists can only be built up from smaller ones,
eventually reaching nil, these two things together establish the
truth of P for all lists l. Here's a concrete example:
Micro-Sermon
Induction on Lists
- First, show that P is true of l when l is nil.
- Then show that P is true of l when l is cons n l' for some number n and some smaller list l', asssuming that P is true for l'.
Theorem app_ass : ∀ l1 l2 l3 : natlist,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
intros l1 l2 l3. induction l1 as [| n l1'].
Case "l1 = nil".
reflexivity.
Case "l1 = cons n l1'".
simpl. rewrite → IHl1'. reflexivity. Qed.
Again, this Coq proof is not especially illuminating as a
static written document — it is easy to see what's going on if
you are reading the proof in an interactive Coq session and you
can see the current goal and context at each point, but this state
is not visible in the written-down parts of the Coq proof. So a
natural-language proof — one written for human readers — will
need to include more explicit signposts; in particular, it will
help the reader stay oriented if we remind them exactly what the
induction hypothesis is in the second case.
Theorem: For all lists l1, l2, and l3,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof: By induction on l1.
Here is an exercise to be worked together in class:
- First, suppose l1 = []. We must show
([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),which follows directly from the definition of ++.
- Next, suppose l1 = n::l1', with
(l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)(the induction hypothesis). We must show((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).By the definition of ++, this follows fromn :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),which is immediate from the induction hypothesis. ☐
Theorem app_length : ∀ l1 l2 : natlist,
length (l1 ++ l2) = (length l1) + (length l2).
Proof.
(* WORKED IN CLASS *)
intros l1 l2. induction l1 as [| n l1'].
Case "l1 = nil".
reflexivity.
Case "l1 = cons".
simpl. rewrite → IHl1'. reflexivity. Qed.
For a slightly more involved example of an inductive proof
over lists, suppose we define a "cons on the right" function
snoc like this...
Fixpoint snoc (l:natlist) (v:nat) : natlist :=
match l with
| nil => [v]
| h :: t => h :: (snoc t v)
end.
... and use it to define a list-reversing function rev
like this:
Fixpoint rev (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => snoc (rev t) h
end.
Example test_rev1: rev [1,2,3] = [3,2,1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.
Now let's prove some more list theorems using our newly
defined snoc and rev. For something a little more challenging
than the inductive proofs we've seen so far, let's prove that
reversing a list does not change its length. Our first attempt at
this proof gets stuck in the successor case...
Theorem rev_length_firsttry : ∀ l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l'].
Case "l = []".
reflexivity.
Case "l = n :: l'".
simpl. (* Here we are stuck: the goal is an equality involving
snoc, but we don't have any equations in either the
immediate context or the global environment that have
anything to do with snoc! *)
Admitted.
So let's take the equation about snoc that would have
enabled us to make progress and prove it as a separate lemma.
Theorem length_snoc : ∀ n : nat, ∀ l : natlist,
length (snoc l n) = S (length l).
Proof.
intros n l. induction l as [| n' l'].
Case "l = nil".
reflexivity.
Case "l = cons n' l'".
simpl. rewrite → IHl'. reflexivity. Qed.
Now we can complete the original proof.
Theorem rev_length : ∀ l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l'].
Case "l = nil".
reflexivity.
Case "l = cons".
simpl. rewrite → length_snoc.
rewrite → IHl'. reflexivity. Qed.
For comparison, here are informal proofs of these two theorems:
Theorem: For all numbers n and lists l,
length (snoc l n) = S (length l).
Proof: By induction on l.
Theorem: For all lists l, length (rev l) = length l.
Proof: By induction on l.
Obviously, the style of these proofs is rather longwinded
and pedantic. After the first few, we might find it easier to
follow proofs that give a little less detail overall (since we can
easily work them out in our own minds or on scratch paper if
necessary) and just highlight the non-obvious steps. In this more
compressed style, the above proof might look more like this:
Theorem:
For all lists l, length (rev l) = length l.
Proof: First, observe that
Which style is preferable in a given situation depends on
the sophistication of the expected audience and on how similar the
proof at hand is to ones that the audience will already be
familiar with. The more pedantic style is a good default for
present purposes.
We've seen that proofs can make use of other theorems we've
already proved, using rewrite, and later we will see other ways
of reusing previous theorems. But in order to refer to a theorem,
we need to know its name, and remembering the names of all the
theorems we might ever want to use can become quite difficult! It
is often hard even to remember what theorems have been proven,
much less what they are named.
Coq's SearchAbout command is quite helpful with this. Typing
SearchAbout foo will cause Coq to display a list of all theorems
involving foo. For example, try uncommenting the following to
see a list of theorems that we have proved about rev:
- First, suppose l = []. We must show
length (snoc [] n) = S (length []),which follows directly from the definitions of length and snoc.
- Next, suppose l = n'::l', with
length (snoc l' n) = S (length l').We must showlength (snoc (n' :: l') n) = S (length (n' :: l')).By the definitions of length and snoc, this follows fromS (length (snoc l' n)) = S (S (length l')),which is immediate from the induction hypothesis. ☐
- First, suppose l = []. We must show
length (rev []) = length [],which follows directly from the definitions of length and rev.
- Next, suppose l = n::l', with
length (rev l') = length l'.We must showlength (rev (n :: l')) = length (n :: l').By the definition of rev, this follows fromlength (snoc (rev l') n) = S (length l')which, by the previous lemma, is the same asS (length (rev l')) = S (length l').This is immediate from the induction hypothesis. ☐
length (snoc l n) = S (length l)
for any l. This follows by a straightforward induction on l.
The main property now follows by another straightforward
induction on l, using the observation together with the
induction hypothesis in the case where l = n'::l'. ☐
SearchAbout
(* SearchAbout rev. *)
Keep SearchAbout in mind as you do the following exercises and
throughout the rest of the course; it can save you a lot of time!
Also, if you are using ProofGeneral, you can run SearchAbout
with C-c C-f. Pasting its response into your buffer can be
accomplished with C-c C-;.
List Exercises, Part 1
Exercise: 3 stars, recommended (list_exercises)
More practice with lists.Theorem app_nil_end : ∀ l : natlist,
l ++ [] = l.
Proof.
(* FILL IN HERE *) Admitted.
Theorem rev_involutive : ∀ l : natlist,
rev (rev l) = l.
Proof.
(* FILL IN HERE *) Admitted.
Theorem distr_rev : ∀ l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
(* FILL IN HERE *) Admitted.
There is a short solution to the next exercise. If you find
yourself getting tangled up, step back and try to look for a
simpler way.
Theorem app_ass4 : ∀ l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
(* FILL IN HERE *) Admitted.
Theorem snoc_append : ∀ (l:natlist) (n:nat),
snoc l n = l ++ [n].
Proof.
(* FILL IN HERE *) Admitted.
An exercise about your implementation of nonzeros:
Lemma nonzeros_length : ∀ l1 l2 : natlist,
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
List Exercises, Part 2
Exercise: 2 stars, recommended (list_design)
Design exercise:- Write down a non-trivial theorem involving cons (::), snoc, and append (++).
- Prove it.
(* FILL IN HERE *)
☐
Exercise: 2 stars, optional (bag_proofs)
If you did the optional exercise about bags above, here are a couple of little theorems to prove about your definitions.Theorem count_member_nonzero : ∀ (s : bag),
ble_nat 1 (count 1 (1 :: s)) = true.
Proof.
(* FILL IN HERE *) Admitted.
The following lemma about ble_nat might help you in the next proof.
Theorem ble_n_Sn : ∀ n,
ble_nat n (S n) = true.
Proof.
intros n. induction n as [| n'].
Case "0".
simpl. reflexivity.
Case "S n'".
simpl. rewrite IHn'. reflexivity. Qed.
Theorem remove_decreases_count: ∀ (s : bag),
ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
☐
There is a hard way and an easy way to solve this exercise.
Exercise: 3 stars, optional (bag_count_sum)
Write down an interesting theorem about bags involving the functions count and sum, and prove it.☐
Exercise: 4 stars, optional (rev_injective)
Prove that the rev function is injective, that is,
∀ X (l1 l2 : natlist), rev l1 = rev l2 → l1 = l2.
(* FILL IN HERE *)
One use of natoption is as a way of returning "error
codes" from functions. For example, suppose we want to write a
function that returns the nth element of some list. If we give
it type nat → natlist → nat, then we'll have to return some
number when the list is too short!
Fixpoint index_bad (n:nat) (l:natlist) : nat :=
match l with
| nil => 42 (* arbitrary! *)
| a :: l' => match beq_nat n O with
| true => a
| false => index_bad (pred n) l'
end
end.
On the other hand, if we give it type nat → natlist →
natoption, then we can return None when the list is too short
and Some a when the list has enough members and a appears at
position n.
Fixpoint index (n:nat) (l:natlist) : natoption :=
match l with
| nil => None
| a :: l' => match beq_nat n O with
| true => Some a
| false => index (pred n) l'
end
end.
Example test_index1 : index 0 [4,5,6,7] = Some 4.
Proof. reflexivity. Qed.
Example test_index2 : index 3 [4,5,6,7] = Some 7.
Proof. reflexivity. Qed.
Example test_index3 : index 10 [4,5,6,7] = None.
Proof. reflexivity. Qed.
This example is also an opportunity to introduce one more
small feature of Coq's programming language: conditional
expressions...
Fixpoint index' (n:nat) (l:natlist) : natoption :=
match l with
| nil => None
| a :: l' => if beq_nat n O then Some a else index (pred n) l'
end.
Coq's conditionals are exactly like those found in any other
language, with one small generalization. Since the boolean type
is not built in, Coq actually allows conditional expressions over
any inductively defined type with exactly two constructors. The
guard is considered true if it evaluates to the first constructor
in the Inductive definition and false if it evaluates to the
second.
The function below pulls the nat out of a natoption, returning
a supplied default in the None case.
Definition option_elim (d : nat) (o : natoption) : nat :=
match o with
| Some n' => n'
| None => d
end.
Exercise: 2 stars (hd_opt)
Using the same idea, fix the hd function from earlier so we don't have to pass a default element for the nil case.Definition hd_opt (l : natlist) : natoption :=
(* FILL IN HERE *) admit.
Example test_hd_opt1 : hd_opt [] = None.
(* FILL IN HERE *) Admitted.
Example test_hd_opt2 : hd_opt [1] = Some 1.
(* FILL IN HERE *) Admitted.
Example test_hd_opt3 : hd_opt [5,6] = Some 5.
(* FILL IN HERE *) Admitted.
Theorem option_elim_hd : ∀ (l:natlist) (default:nat),
hd default l = option_elim default (hd_opt l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, recommended (beq_natlist)
Fill in the definition of beq_natlist, which compares lists of numbers for equality. Prove that beq_natlist l l yields true for every list l.Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
(* FILL IN HERE *) admit.
Example test_beq_natlist1 : (beq_natlist nil nil = true).
(* FILL IN HERE *) Admitted.
Example test_beq_natlist2 : beq_natlist [1,2,3] [1,2,3] = true.
(* FILL IN HERE *) Admitted.
Example test_beq_natlist3 : beq_natlist [1,2,3] [1,2,4] = false.
(* FILL IN HERE *) Admitted.
Theorem beq_natlist_refl : ∀ l:natlist,
true = beq_natlist l l.
Proof.
(* FILL IN HERE *) Admitted.
Module Dictionary.
Inductive dictionary : Type :=
| empty : dictionary
| record : nat → nat → dictionary → dictionary.
This declaration can be read: "There are two ways to construct a
dictionary: either using the constructor empty to represent an
empty dictionary, or by applying the constructor record to
a key, a value, and an existing dictionary to construct a
dictionary with an additional key to value mapping."
Below is a function find that searches a dictionary for a
given key. It evaluates evaluates to None if the key was not
found and Some val if the key was mapped to val in the
dictionary. If the same key is mapped to multiple values, find
will return the first one it finds.
Fixpoint find (key : nat) (d : dictionary) : natoption :=
match d with
| empty => None
| record k v d' => if (beq_nat key k) then (Some v) else (find key d')
end.
(* Complete the following proof. *)
Theorem dictionary_invariant1 : ∀ (d : dictionary) (k v: nat),
(find k (insert k v d)) = Some v.
Proof.
(* FILL IN HERE *) Admitted.
Theorem dictionary_invariant1 : ∀ (d : dictionary) (k v: nat),
(find k (insert k v d)) = Some v.
Proof.
(* FILL IN HERE *) Admitted.
(* Complete the following proof. *)
Theorem dictionary_invariant2 : ∀ (d : dictionary) (m n o: nat),
(beq_nat m n) = false → (find m d) = (find m (insert n o d)).
Proof.
(* FILL IN HERE *) Admitted.
Theorem dictionary_invariant2 : ∀ (d : dictionary) (m n o: nat),
(beq_nat m n) = false → (find m d) = (find m (insert n o d)).
Proof.
(* FILL IN HERE *) Admitted.
☐


Daily Digest #63
- Part 2: Rate Limiting for API gateways
- the ultimate postgres vs mysql blog post – for a while..
- Postgres Internals: Building a Description Tool
- Is Your Postgres Query Starved for Memory? – old post, but still relevant for everyday use
- Beyond ‘Punk Rock Git’ in Eleven Steps
- Five microservice testing strategies for startups
Daily Digest #62
- Slicker: A Tool for Moving Things in Python tool
- Extracting Signals From the News
- Information Theory of Neural Networks
- Why junior devs should review seniors’ commits
- Builders of the Decentralized Web: 10 Of The Most Innovative Technologies
- Part 1: Rate Limiting: A Useful Tool with Distributed Systems
Daily Digest #61
- Safe ways to do things in bash – we all did it, aren’t we?
- Compromising: A Guide for Developers
- 27 things I learned about hiring in tech from looking for a new engineering management role
- The Comprehensive Beginner’s Guide to JavaScript Geolocation Tracking
- Introducing DNS Resolver, <IP_ADDRESS> (not a joke)
- Phones, Lambdas and the Joy of Snap-to-Place Technology


Statistics:
"Created by" statistics:
Number of Projects: 0
Number of Tasks: 0
Number of Avg Tasks per Project: 0
Number of "ToDo" Tasks: 0
Number of "InProgress" Tasks: 0
Number of "Done" Tasks: 0
Number of "Expired" Tasks: 0
"Working On" statistics:
Number of Tasks: 0
Number of "InProgress" Tasks: 0
Number of "Done" Tasks: 0
Number of "Expired" Tasks: 0


Safe Numerics |
This holds an arithmetic value which can be used as a replacement for built-in C++ arithmetic values. These types differ from their built-in counter parts in that the are guaranteed not to produce invalid arithmetic results. These operations return safe types rather than built-in types.
| Symbol | Description |
|---|---|
T, U |
Types fulfilling Numeric type requirements |
| t, u | objects of types T, U |
| S, S1, S2 | A type fulfilling SafeNumeric type requirements |
| s, s1, s2 | objects of types S |
| op | C++ infix operator |
| prefix_op | C++ prefix operator: -, +, ~ |
| postfix_op | C++ postfix operator |
| assign_op | C++ assignment operator |
| Expression | Result Type | Description |
|---|---|---|
s op t |
unspecified S | invoke safe C++ operator op and return another SafeNumeric type. |
t op s |
unspecified S | invoke safe C++ operator op and return another SafeNumeric type. |
s1 op s2 |
unspecified S | invoke safe C++ operator op and return another SafeNumeric type. |
prefix_op S |
unspecified S | invoke safe C++ operator |
S postfix_op |
unspecified S | invoke safe C++ operator |
s assign_op t |
S1 | convert t to type S1 and assign it to s1. If the value t cannot be represented as an instance of type S1, it is an error. |
S(t) |
unspecified S | construct an instance of S from a value of type T. If the value t cannot be represented as an instance of type S1, it is an error. |
S |
S | construct an uninitialized instance of S. |
is_safe<S> |
std::true_type or
std::false_type
|
type trait to query whether any type T fulfills the requirements for a SafeNumeric type. |
static_cast<T>(s) |
T | convert the value of s to type T. If the value of s cannot be correctly represented as a type T, it is an error. Note that implicit casting from a safe type to a built-in integer type is expressly prohibited and should invoke a compile time error. |
The result of any binary operation where one or both of the operands is a SafeNumeric type is also a SafeNumeric type.
All the expressions in the above table are
constexpr
expressions
Binary expressions which are not assignments require that promotion and exception policies of the operands be identical.
|
, &
, ^
and
~
operations defined for safe signed integer types. It's
not clear that this is the correct decision. On one hand, usage of
these operators on signed types is almost certainly an error in
program logic. But trapping this as an error conflicts with the goal
of making safe types "drop-in" replacements for the corresponding
built-in types. In light of this, these operators are currently
supported as they are for normal built-in types.
Safe Numeric operators will NOT perform standard numeric conversions in order to convert to built-in types.
void f(int); int main(){ long x; f(x); // OK - builtin implicit version safe<long> y; f(y); // compile time error return 0; }
This behavior prevents a safe<T>
from
being a "drop-in" replacement for a T
.
There are no complexity guarantees explicitly enforced here. However, it would be very surprising if any implementation were to be more complex that O(0);
The fundamental requirement of a SafeNumeric type is that it implements all C++ operations permitted on its base type in a way the prevents the return of an incorrect arithmetic result. Various implementations of this concept may handle circumstances which produce such results differently (throw exception, compile time trap, etc..) no implementation should return an arithmetically incorrect result.


--- layout: post title: Fmask and dmask author: Galuh D Wijatmiko categories: [Troubleshot] tags: [Linux] ---
umask is set to controld permissions (set by the server administrator) for newly created files & directories. That is created by other users on the system.When you set a umask for example 0666 then you need to minus this 0666 with 0777 for a directory and 0666 for files.
And then you get a system umask of 0111. 0666 - 0777 = 0111 for your directoryes, and 0555 for your files.The directory number to minus your umask with is 0777 and
the files number to minus your umask with is 0666Another example. Directory.
0222 - 0777 = 0555
0274 - 0777 = 0503and Files.
0222 - 0666 = 0444
0264 - 0666 = 0402a umask 0000 is = 0777 = all permissions
Read
Write
Executea umask 0111 is = 0666 = Read + WriteWhen looking at permissions you seex xxx xxx xxx
x = Type (directory, file, special files e.c.t)
#1 xxx = users
#2 xxx = groups
#3 xxx = othersThese 3 x then has a value.
4 2 1 4 2 1 4 2 1
X X X X X X X X X
R W X R W X R W XR = Read
W = Write
X = Executethe value 7 is all the numbers in a XXX group put together 4+2+1 = 7 = all permissions.If it was 0752 then it would be
#1 Users = all permissions 4+2+1 = 7
#2 Groups = Write + Execute 4+1 = 5
#3 Others = Write 2 = 2Hope this helpsADDED:
For the first digit in a umask. Its a sticky bit.(4)xxx sets the SUID
(2)xxx sets the SGID
(1)xxx sets the sticky bit
(6)xxx sets both the SUID and SGID
(7)xxx sets all three The sticky bit does if more people (a group) has 0777 permissions to a file, then they can delete the file also. If i want
them to have all permissions but not able to delete the file i can set a sticky bit 1777 and then its only the owner of the file who can delete it. The group can still see the file, open it, change its contents. They can do all that the permissions alow them to EXECT deleting the file.And then the permissions would look like this rwx-rwx-rwt the t reporsents the sticky bit. A umask of 1777
“fmask=177,dmask=077” “Root has read/write access, users have no access”“fmask=333,dmask=222” “Everyone has read only access”“fmask=133,dmask=022” “Everyone has read access, but only root can write”“fmask=111,dmask=000” “All users can read/write to any file”References : http://ubuntuforums.org/showthread.php?t=1453342


FOR CENTURIES, PLANETS beyond our solar system called exoplanets existed only in theory and science fiction. It seemed nearly impossible to detect planets light-years away, since the relatively tiny worlds would appear billions of times fainter than their parent stars. But in the last two decades astronomers have successfully developed indirect detection methods, most of which rely on measuring the effects of orbiting planets on far-off stars.
In 1992 astronomers reported the first planet-size masses around a dead star, the pulsar PSR1257+12, which sits 2,000 light-years away. Three years later came news of the first known exoplanet, a Jupiter-like gas giant orbiting its star closer than Mercury circles our sun. That world was detected around the sunlike star 51 Pegasi, a mere 50 light-years from Earth.
The rate of exoplanet discovery has since climbed rapidly thanks to the development of three main detection techniques, which all involve both ground- and space-based observatories. As of January 2012, the tally of confirmed alien worlds has skyrocketed to just over 720. However, the hunt is still on for a truly Earthlike planet, one with the right size, temperature, and composition to host liquid water—and maybe life.
The most successful planet-hunting technique to date has been radial velocity, also called the Doppler wobble, with more than 400 newfound planets to its credit. Astronomers using this method look for a star's “wobble”—telltale shifts in a star's light spectrum—caused by the gravitational tugs of orbiting planets. The more massive a planet and the tighter its orbit, the greater its effect on the host star. As a result, the majority of discoveries made with this method have been so-called hot Jupiters, because of their large masses and close proximities to their parent stars.
Nearly two dozen planets have been detected using the microlensing technique, starting with the 2003 discovery of a gas giant twice the size of Jupiter orbiting a star 18,000 light-years away. Gravitational microlensing occurs when one star passes directly in front of a background star, as seen from Earth. The gravitational field of the foreground star acts like a lens, magnifying the light of the background star. If the “lens” star has an orbiting planet, the extra mass amplifies the magnification in a telltale way.
The transit method, another popular technique, looks for periodic dips in a star's brightness as an orbiting planet passes in front of—or transits—its star, as seen from Earth. By measuring the amount and frequency of a star’s dimming, astronomers can estimate the orbits and masses of its planets. Additionally, researchers can calculate a planet’s surface temperature from the world’s orbital period and its star’s temperature.
Since its launch in 2009, NASA's Kepler mission has used the transit method to confirm more than 60 new exoplanets and to identify 2,300 candidate planets now awaiting confirmation via further observations. Monitoring more than 150,000 stars, the planet-hunting spacecraft is the first built that’s capable of detecting Earth-size worlds in a sunlike star’s habitable zone, the region around a star where liquid water—and maybe life—can exist.
As of early 2012, Kepler has uncovered 17 stars with multiple planets as well as a new class of planets that orbit double and even triple stars. But only a handful of the exoplanets discovered so far are terrestrial, rocky types like Earth, and very few are in their stars’ habitable zones. For instance, three of the smallest rocky exoplanets yet detected—each no larger than Mars—closely orbit the red dwarf star KOI-961 and are far too hot to host life.
Calculations based on initial data from Kepler suggest that a hundred billion planets exist in the Milky Way galaxy. Of those, as many as ten billion may be rocky planets like Earth. Future searches with improved monitoring technology are expected to reveal ever smaller exoplanets, worlds that orbit at larger distances from their parent stars, and even alien moons.
Based on the progress made so far, some experts think we’ll find the first truly Earthlike planets in the next year or two. By combining information from radial velocity and transit methods, for instance, astronomers will be able to determine the compositions of an Earth-size planet’s atmosphere and search for telltale signs of life, such as oxygen and methane gases.


Welcome to the Discworld Disorganiser.
This application is designed to be a book and character search engine interface for the Discworld series of books.
To use this application, click on either 'Books', 'Characters' or 'Series', these will take you to a search screen where you can search for a book, character or series within the Discworld canon
This application runs on .NET Core and Angular2, with TypeScript compiled client-side scripting
The search functionality is provided by my dwCheckApi project. The source code for dwCheckApi can be found here


Disadvantages of Dependency injection
(In the Java world)
- can make code difficult to trace (separates behaviour from construction) - see a Spring stack trace,
Dagger 2 - tries to avoid this
- typically requires more lines of code
- diminishes encapsulation
- some performance impact due to use of reflection - again Spring, Dagger 2


Task Manager is a web app that allows users to create lists or tasks and add and remove content for each of those tasks. Each user has their own lists with content so registration is required


|
Bitstream Interpretation Library (BIL)
0.1
|
Contains declaration of IOException class. More...
#include <exception/Exception.hpp>
Go to the source code of this file.
Classes | |
| class | bil::IOException |
| Exception for I/O errors. More... |
Namespaces | |
| namespace | bil |
Macros | |
| #define | BIL_IOEXCEPTION_HPP |
Contains declaration of IOException class.
Definition in file IOException.hpp.
| #define BIL_IOEXCEPTION_HPP |
Definition at line 8 of file IOException.hpp.


--- locale: "en" ---
Hungry to offer their talents towards a public cause, the attendees of ReRouteAVL’s Friday night community brainstorm made their case for a variety of potential alternatives to single passenger car-based transit. Organized by Code for Asheville, a local Code for America brigade, ReRouteAVL was held in a team-based competitive format, pitting local talent against local talent in a friendly and productive atmosphere. ReRouteAVL provided an opportunity for developers, engineers, designers, writers, organizers, and activists to showcase their talents and make a public impact in their own city. During Friday’s open forum at Mojo coworking, professionals from a multitude of backgrounds and disciplines offered their thoughts on technological possibilities to make alternative forms of transportation safer and more efficient. Solutions for carpooling, traffic density issues, parking, and bus locating were just a few of the many proposals submitted for consideration.
AVLRide: Carpooling Made Easy (http://www.avlride.com/):
A neighborhood approach to carpooling to connect people who live in the same area and want to carpool to work in the same area.
Where’s My Bus? (http://avlbus.com):
A nice mashup of NextBus real time bus data with Google Map directions so that a user can both see bus locations in real time and plan a route to a destination with that real time data.
Safe Route (link coming):
Statistical analysis of bike and pedestrian crash data to show which intersections and areas are particularly dangerous as well as the times of data that are most dangerous; huge potential for policy makers to improve safety of designated dangerous intersections
Getthere.io (link coming):
Brainstorming and Paper Prototyping around transportation issues facing festival attendees.
MapMyMode (link coming):
Multi-modal map routing with the ability to provide comments about portions of cycling and walking routes. It also allows users to decide on the most important criteria for their trip - speed, cost, difficulty (e.g. steep terrain), or how scenic the route will be.
Thank you to all who attended! Want to stay involved? Here's some next steps.
ReRoute AVL has received great coverage, both nationally and locally!
If you'd like to know more about ReRoute AVL, or would like to get in contact with a specific project team, please contact Patrick Conant


Xcode 5 introduced a host of new features, fixes and performance enhancements but it also makes it possible to simplify your Xcode project and discard some maintenance tasks.
Every Xcode project you’ve worked with is likely to have a Frameworks group at the root of the project. If you’re on OS X it might contain things like Cocoa.framework, Foundation.framework and CoreData.framework, on iOS it holds UIKit.framework and friends. One of the improvements that came with Xcode 5 was LLVM Modules. One of the improvements that modules brings is the ability to automatically link any system frameworks that you #import
. This is awesome, and it’s one less thing you now have to look after.
As long as you’re only keeping system frameworks in that group, you can delete it. Yes, delete the entire “Frameworks” group. Just ensure that you’ve enabled Link Frameworks Automatically in your Xcode project’s settings.
If you’re on iOS, you will need to ensure that “Enable Modules (C and Objective-C)” is also set “Yes” or this tip won’t work. OS X works either way. Thanks to Chris Wood for pointing this out
When you open up your project’s schemes menu, do you see a bunch of schemes from third party projects in there?
To clean them up, go to Product → Scheme → Manage Schemes… and uncheck Show for any that you don’t want to see.
The caveat is that unless you check the “Shared” column, these settings will be reset if your user project settings are ever reset. It’s easy enough to reapply.
Older projects often show schemes for any unit test bundles you have in your project — you don’t actually need to show them at all!
It was necessary under Xcode 4 to have separate schemes for your test targets so that CI servers could find and run them (
xcodebuild
didn’t support the “test” action until Xcode 5).
As long as your test targets specify their Target Dependencies properly, you can just go to Product → Scheme → Manage Schemes… and delete any test schemes that are listed.
Wow, what an improvement. And no loss of functionality!
This is a simple one, but manually ordering your classes and groups is one way to waste a lot of time. Why not just right click on a group/project in the Xcode navigator and select Sort Files By Name?
Hopefully these tips have helped you clean up your Xcode project a little. Hopefully you’ve also removed a few things you don’t really need to see from your line of sight, freeing up a little bit of brain power for something else!


Secant Method¶
Newton Raphson is good general purpose root finding method, but sometimes if function is very complicated then computing derivates will take much computational time, so to overcome this issue, in secant method we approximate the first order derivative term f’(r). Algorithm is more or less similar to secant method
Given an equation f(x) = 0
Let the initial guesses be x0 and x1
Do
xi+1= xi - ( f(xi) * (xi - xi-1) ) / ( f(xi) - f(xi-1) )
while (none of the convergence criterion C1 or C2 is met)
Convergence criterias are:-
- C1. Fixing apriori the total number of iterations N.
- C2. By testing the condition \(| x_{i+1} - x_i |\) (where i is the iteration number) less than some tolerance limit, say epsilon, fixed threshold.
C Implementation¶
#include<stdio.h>
#include<math.h>
#define f(x) (pow(x,3)-18)
int main(){
float x0,x1,x2,error;
int i=0;
printf("Input Two Approximations: ");
scanf("%f %f",&x0,&x1);
printf("Ite\tX0\t\tX1\t\tf(X0)\t\tf(X1)\t\tError\n");
do{
x2=((x0*f(x1))-((x1)*f(x0)))/((f(x1)-f(x0)));
printf("%2d\t%4.6f\t%4.6f\t%4.6f\t%4.6f\t%4.6f\n",i++,x0,x1,f(x0),f(x1),error);
error=fabs((x2)-(x1));
x0=x1;
x1=x2;
}while(error>0.00005);
return 0;
}
Output¶
Input Two Approximations: 1 2
Ite X0 X1 f(X0) f(X1) Error
0 1.000000 2.000000 -17.000000 -10.000000 0.000000
1 2.000000 3.428571 -10.000000 22.303208 1.428571
2 3.428571 2.442238 22.303208 -3.433201 0.986333
3 2.442238 2.573814 -3.433201 -0.949728 0.131575
4 2.573814 2.624131 -0.949728 0.069927 0.050317
5 2.624131 2.620680 0.069927 -0.001263 0.003451
6 2.620680 2.620741 -0.001263 -0.000001 0.000061
With this discussion, this series on solution of non linear equations with Iterative Methods concludes.


Send Message


|
Figure 1
|
Top (left) and side (right) views of 1. Gd, Purple; W, mediu ... |
|
Figure 2
|
Zeeman energy scheme of 1 as a function of the applied magne ... |
|
Figure 3
|
Calculated and experimental phase memory times T m of 1 at e ... |
|
Figure 4
|
View of 1 surrounded by the crystallographic positions of so ... |