PCC116 - Agda Library

A simple Agda library developed during the course PCC116 - Logics in computer science at Universidade Federal de Ouro Preto.

Exercises

• Lista 04 - Definições e teoremas sobre booleanos

  • Data para entrega: 09/10/2021, pela plataforma Moodle.
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Bool/Bool.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Bool/BoolTheorems.agda

• Lista 05 - Definições e teoremas sobre números naturais.

  • Data para entrega: 16/10/2021, pela plataforma Moodle.
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/Le.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/LeAlt.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/NatTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/EvenOdd.agda

• Lista 06 - Lógica em Agda, Evidências.

  • Data para entrega: 23/10/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Product/ProductTheoerms.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Sum/SumTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Biconditional/BiconditionalTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Relation/Decidable/Dec.agda

• Lista 07 - Listas e funções de ordem superior.

  • Data para entrega: 30/10/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/ListTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Relation/All.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Relation/Any.agda

• Lista 08 - Programação com tipos dependentes - Parte I.

  • Data para entrega: 06/11/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Vec/Vec.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Vec/Matrix.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Language/Data/Data.agda

• Lista 09 - Programação com tipos dependentes - Parte II.

  • Data para entrega: 13/11/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Relation/Sublist.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Sorting/Extrinsic/StalinSort.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Sorting/Extrinsic/StalinSortTheorems.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/List/Sorting/Intrinsic/InsertionSort.agda

• Lista 10 - Recursão não estrutural.

  • Data para entrega: 20/11/2021
  • Formato de entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Nat/Div/DivIntrinsic.agda

• Lista 11 - Noções de semântica formal.

  • Data para entrega: 27/11/2021
  • Formato para entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib.
  • Arquivos contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Language/Exp/Intrinsic.agda
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Language/Exp/Extrinsic.agda

• Lista 12 - Programação genérica.

  • Data para entrega: 04/12/2021
  • Formato para entrega: arquivo .zip contendo todo o código da biblioteca pcc116-agda-lib
  • Arquivo contendo os exercícios da lista:
    • https://github.com/rodrigogribeiro/pcc116-agda-lib/blob/master/Data/Generic/GSize.agda

Installation

For installing the library, please consult the instalation instructions at

https://agda.readthedocs.io/en/v2.6.2/tools/package-system.html