michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Updated to stdlib version 0.17

Browse source
This commit is contained in:
Wen Kokke 2018-12-18 11:46:25 +00:00
parent a4c207c1ce
commit ea2398ec0e
3 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.travis.yml
View file

@ -13,7 +13,7 @@ cache:
- $HOME/.agda - $HOME/.agda
- $HOME/.local - $HOME/.local
- $HOME/agda-$AGDA_VERSION - $HOME/agda-$AGDA_VERSION
- $HOME/agda-stdlib-master - $HOME/agda-stdlib-$AGDA_STDLIB_VERSION
- $HOME/agda2html-master - $HOME/agda2html-master
- $HOME/acknowledgements-master - $HOME/acknowledgements-master

16
Makefile
View file

@ -81,7 +81,7 @@ travis-setup:\
$(HOME)/.local/bin/agda\ $(HOME)/.local/bin/agda\
$(HOME)/.local/bin/agda2html\ $(HOME)/.local/bin/agda2html\
$(HOME)/.local/bin/acknowledgements\ $(HOME)/.local/bin/acknowledgements\
$(HOME)/agda-stdlib-master/src\ $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
$(HOME)/.agda/defaults\ $(HOME)/.agda/defaults\
$(HOME)/.agda/libraries $(HOME)/.agda/libraries
@ -132,7 +132,7 @@ $(HOME)/.agda/defaults:
echo "plfa" >> $(HOME)/.agda/defaults echo "plfa" >> $(HOME)/.agda/defaults
$(HOME)/.agda/libraries: $(HOME)/.agda/libraries:
echo "$(HOME)/agda-stdlib-master/standard-library.agda-lib" >> $(HOME)/.agda/libraries echo "$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/standard-library.agda-lib" >> $(HOME)/.agda/libraries
echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries
$(HOME)/.local/bin/agda: $(HOME)/.local/bin/agda:
@ -151,15 +151,17 @@ travis-reinstall-agda: travis-uninstall-agda travis-install-agda
.phony: travis-install-agda travis-uninstall-agda travis-reinstall-agda .phony: travis-install-agda travis-uninstall-agda travis-reinstall-agda
travis-install-agda-stdlib: $(HOME)/agda-stdlib-master/ travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/
$(HOME)/agda-stdlib-master/src: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src:
curl -L https://github.com/plfa/agda-stdlib/archive/master.zip -o $(HOME)/agda-stdlib-master.zip curl -L https://github.com/plfa/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip -o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
unzip -qq $(HOME)/agda-stdlib-master.zip -d $(HOME) unzip -qq $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip -d $(HOME)
mkdir -p $(HOME)/.agda mkdir -p $(HOME)/.agda
travis-uninstall-agda-stdlib: travis-uninstall-agda-stdlib:
rm -rf $(HOME)/agda-stdlib-master/ rm $(HOME)/.agda/defaults
rm $(HOME)/.agda/libraries
rm -rf $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/
travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib

2
src/plfa/Decidable.lagda
View file

@ -556,7 +556,7 @@ postulate
\begin{code} \begin{code}
import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not) import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
import Data.Nat.Base using (_≤?_) import Data.Nat using (_≤?_)
import Data.List.All using (All; []; _∷_) renaming (all to All?) import Data.List.All using (All; []; _∷_) renaming (all to All?)
import Relation.Nullary using (Dec; yes; no) import Relation.Nullary using (Dec; yes; no)
import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness) import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)