summaryrefslogtreecommitdiff
path: root/src/Obs/Main.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2023-01-12 17:57:06 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2023-01-12 17:57:06 +0000
commit72feeec46c34c678640341e76958481f4244d8df (patch)
tree3480dc151716912ffd2bba6d21bcc69798f844b9 /src/Obs/Main.idr
parentbfba6b295a8cdf7321d939f22fbdd04d45408e63 (diff)
Provide examples of Obs code.HEADmaster
This folder spells out the action of equality and cast for the different type constructors. Ideally the two correctness proofs should given by reflexivity.
Diffstat (limited to 'src/Obs/Main.idr')
0 files changed, 0 insertions, 0 deletions