Day 3 Of Learning Lean 4

Day 3 of learning Lean 4

Types are 2 Dimensional

that is all

Learning Haskell as my second language has heavily skewed my perspective on programming.

Powershell syntax is not confusing

(you are just confused because posix compliant shells have corrupted your mind)

> do-action -param "string" $variable (do this first) [type]value

To declare a function:

function do-mythings {

param([int]$argument)

$argument + 5

}

> do-mythings -arg 5

10

That's all you need to get started.

Numbers are just numbers.

Inline math just works. Parentheses for order of operations.

Strings you put in quotes - double quotes allow interpolation, single quotes don't. This is the same as sh.

All variables are prefixed with $s. Even when declaring them. This makes slightly more sense than sh.

A region in {squirrelly braces} gets the [scriptblock] data type. It's like a lambda but comprehensible by mere mortals.

if (test) {success} else {fail} - the test is always executed first because (). Success and fail conditions only depending on the test. They're script blocks. No weird special syntax, if may as well be a user function.

Functions can be named anything, but the convention is Verb-PlaceThing. Not case sensitive.

Named arguments are specified with a single hyphen, like MIT Unix software (xorg for instance). If there is only one parameter the name is optional, etc. Param names can be abbreviated as long as they aren't ambiguous. This is also easy to follow with your own functions, unlike in sh (fricking hate getopt).

Types are inferred dynamically because it's easier to write scripts that way. If you need to force something (variable, expression, whatever) to have a specific type, put it in [brackets] beforehand. The type names are the same as c# and every other post-algol language. For comparison, posix shell only has one type, String.

To make an array, @(item1, item2, etc)

To make a hashtable, @{

key1 = val1

key2 = val2

}

Adding strings concatenates them together. Adding numbers adds their values. If this is not satisfactory, declare their types and it will work.

All expressions are technically objects with properties and methods. $var.property returns the value of that property. $var.invokeMethod() runs the method, which is just a function built into that data type by some poor intern 20 years ago.

Pipes (|) work similarly to sh, but transfer objects. The current object in the pipeline is always the variable $_.

As a bonus, here's a one-liner for opening Internet Explorer on Windows 11 (they lied, it's still there, they will never remove it)

(new-object -com "InternetExplorer.application").visible = $true

COM is an old windows api. Com Objects are just instances of apps. We open internet explorer as a com object.

The parentheses sets that as an expression, and its return value _is_ the exploder. It has properties like visibility, which is $false by default. This is boring so set it to $true. Now we have a real working instance of an app they've been trying to remove for years, because they can't actually remove it merely hide it away. As long as the windows api can parse HTML, this will still work.

Does anyone have any objections??

Anyone else learn languages designed to be proof assistants? Or atleast designed with theorem proving as a usecase. Whilst barely knowing any pure Math?

When I first started learning Idris2, I had no idea how to even structure a proof. Needless to say I was quite lost, even if I was experienced in Haskell at that point.

Even now when I'm learning Lean, when I started which was about 5 days ago, I only knew how to prove with truth tables. It wasn't until yesterday when I found about the logics other than Classical.

So basically all I know about pure math is just me brute-forcing my way into learning languages like Idris as well as the occasional Haskell article or codewars kata ethat deep dives into a concept.

It wasn't until recently when I decided to finally sit down and learn Pure Math starting from basic Discrete Math. It's fun because I keep recognizing the concepts that's become commonplace in the languages I use. I learned about Connection intros and eliminations before knowing the difference between classical and intuitionistic logic.

What I'm saying is I love Curry-Howard correspondence