Skip to content

Draft: small proofs to pick up the ropes

corneliuhoffman requested to merge small-proofs into master

This is my first attempt, not sure it should be merged. It includes the following:

  • definitions for last and last_opt in Environments/List.v
  • a new file Proofs/List.v with 3 lemmas.
Edited by Guillaume Claret

Merge request reports