Skip to content

README.md

Latest commit

 

History

History
34 lines (31 loc) · 1.02 KB

README.md

File metadata and controls

34 lines (31 loc) · 1.02 KB

Variations on Noetherianness

This repository contains the Agda code associated with the paper "D. Firsov, T. Uustalu, N. Veltri. Variations on Noetherianness" published at MSFP 2016.

Contents

  • Definitions of notions of finiteness
    • Listable.agda
    • Noetherian.agda
    • Streamless.agda
    • Bounded.agda
    • AlmostFull.agda
  • NoethExamples.agda - examples of noetherian sets
  • Properties of notions of Noetherianness
    • NoethAccDecEq.agda -- NoethDecEq
    • NoethRels.agda -- NoethAcc→NoethAccS -- NoethAccS→NoethSet -- NoethSet→NoethAccS -- NoethAccS→NoethGame -- NoethExposeX→Listable
    • StreamlessProps.agda -- NoethAccS→StreamlessS -- NoethAcc→Streamless
    • AlmostFullProps.agda -- AFEq→NoethAcc -- NoethAcc→AFEq
  • Separating notions
    • NotNotIn.agda -- separating NoethAcc from NoethAccS
    • MaybeProp.agda -- separating NoethExpose from Bounded
    • PropSet.agda -- separating Listability from NoethExpose

Setup

Agda @ 2.6.0.1, agda-stdlib @ 1.1-1