project-pterodactyl/Sources/PterodactylCore/ at push-llryukwrwlqq · jonmsterling.com/project-pterodactyl · Tangled

jonmsterling.com / project-pterodactyl

5

This repository has no description www.jonmsterling.com/01HC/

dependent-types proof-assistant swift

5

project-pterodactyl / Sources / PterodactylCore /

at push-llryukwrwlqq 5 folders 7 files

Jon Sterling Getting program declarations working 5mo ago

Simplify all the thunking

5 months ago

Getting program declarations working

5 months ago

Finish incomplete refactor of InvertedSubst

5 months ago

Local Environments

ProgramLhs: erase the local names

5 months ago

Getting program declarations working

5 months ago

Mitigating the “Goodbye Lenin” problem To do, I had to disable dubbing for distillation. This will be solved otherwise soon.

5 months ago

EnrichSpine.swift

Mitigating the “Goodbye Lenin” problem To do, I had to disable dubbing for distillation. This will be solved otherwise soon.

5 months ago

Remove unnecessary keyword arguments

5 months ago

Evaluator.swift

Add "pattern mode" to environment, unify Identifier with PatternMeta One current defect is that Identifier in synthesis mode cannot produce a pattern meta of a large type, because unification cannot resolve large types. This probably should be addressed by making the mode switch more subtle.

5 months ago

Mitigating the “Goodbye Lenin” problem To do, I had to disable dubbing for distillation. This will be solved otherwise soon.

5 months ago

Preparing for labelled introduction rules, etc.

5 months ago

Quotation.swift

Add named program tactic This lets you do something basically like fun identity (T : Type) (t : T) : T where identity A x => x to produce the \A x => x. This is not a declaration: it's a local form that will be used as part of the declaration mechanism.

5 months ago