Most of what I know about LaTeX is just from having used other people's snippets and random stack overflow answers and I feel like I should probably one day read, like, whatever the official reference guide for LaTeX

I'm tired of this it's so tedious
I'm sure the subsizing judgement translates to a proof of ≤
But I gotta have all my pieces ready eventually, and if I don't do it now I still have to do it later...

Agda vs. in LaTeX
Sure is wordy without all the nice implicits

If Agda people can manage `suc`/`lsuc` then people reading this can manage `suc`/`succ`

Would it be confusing to have both `suc` and `succ`, and then both `lim` and `limit`

I would call it "limit" but the other constructor that states that the upper bound is the least upper bound is named "limiting" so idek anymore

I need to name the constructors of my order but the paper I'm following calls it "cocone" and I don't know what that means

Take an undecidable proof search
Sometimes you can't find the proof because its negation holds so you're spending all your time looking for something that isn't there
Sometimes you can't find the proof because there just isn't any term that proves it, or refutes it, or even irrefutes it

You ever think about how undecidability sometimes means independence

Sometimes... It's clearer to describe syntactic sugar using words than using symbols in a pseudometafunction...

Society has moved beyond the need for fully-sized inductives

Setzt du dich auch bitte endlich hin?

help it's running off the page

Oh I see. The paper restrict what may be declared as a Prop but the implementation allows anything in Prop and then disallows pattern matching

Alright I'm very suspicious of whether Agda checks Prop by default because I can put naturals in Prop and that's very disallowed by the definitional proof irrelevance paper

I can do this too:

``data Pair (A : Set ℓ) (B : A → Set ℓ) : Prop ℓ where  pair : (a : A) → B a → Pair A B``

Wasn't there something not good with strong pairs in Prop? Maybe that was only for impredicative Prop? Odd that definitionally strict Prop is fine

Agda lets me put W types in Prop as long as its level is the same as the parameter universe levels, even if the parameters are in Set
Weird

`sudo rm -rf / --no-preserve-root`

``bundle exec rails assets:clobberbundle exec rails assets:precompile``
Show older

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.