yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Remove the badge
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Yiyun Liu 2025-07-08 16:31:29 -04:00
parent a284102b02
commit b9f165045a
2 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
Makefile
View file

@ -15,10 +15,13 @@ install: $(COQMAKEFILE)
uninstall: $(COQMAKEFILE)
$(MAKE) -f $(COQMAKEFILE) uninstall
export:
git archive --output supplementary.tar master --prefix supplementary/source/
theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
.PHONY: clean FORCE
.PHONY: clean FORCE export
clean:
test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )

2
README.org
View file

@ -1,6 +1,4 @@
* Mechanization of decidable type conversion with surjective pairing
[[https://woodpecker.electriclam.com/api/badges/3/status.svg]]
This repository contains a mechanized proof of decidable type
conversion for a dependent type theory with a cumulative universe
hierarchy, subtyping (contravariant on functions), natural numbers