From bb55c027cada60f527e5301a6560bda40ca47c3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Laurent?= Date: Wed, 12 Jul 2023 11:03:03 +0200 Subject: [PATCH] fix link in README --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c78165b..e5766c7 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ Presentation This repo contains the formalisation work accompangy the paper *Definitional Functoriality for Dependent (Sub)Types*. -The formalisation follows a similar [Agda formalization]((https://github.com/mr-ohman/logrel-mltt/)) (described in [*Decidability of conversion for Type Theory in Type Theory*, 2018](https://dl.acm.org/doi/10.1145/3158111)). In order to avoid some work on the syntax, this project uses the [AutoSubst](https://github.com/uds-psl/autosubst-ocaml) project to generate syntax-related boilerplate. It also includes code from Winterhalter's [partial-fun](https://github.com/TheoWinterhalter/coq-partialfun) library to handle the definition of partial functions. +The formalisation follows a similar [Agda formalization](https://github.com/mr-ohman/logrel-mltt/) (described in [*Decidability of conversion for Type Theory in Type Theory*, 2018](https://dl.acm.org/doi/10.1145/3158111)). In order to avoid some work on the syntax, this project uses the [AutoSubst](https://github.com/uds-psl/autosubst-ocaml) project to generate syntax-related boilerplate. It also includes code from Winterhalter's [partial-fun](https://github.com/TheoWinterhalter/coq-partialfun) library to handle the definition of partial functions. Building =========== @@ -59,4 +59,4 @@ Rather than building the derivation of conversion by hand, we use our certified [BundledAlgorithmicTyping]: ./theories/BundledAlgorithmicTyping.v [AlgorithmicTypingProperties]: ./theories/AlgorithmicTypingProperties.v [Decidability]: ./theories/Decidability.v -[Example_1_1]: ./theories/Example_1_1.v \ No newline at end of file +[Example_1_1]: ./theories/Example_1_1.v