Skip to content
Snippets Groups Projects
Commit 5ddd2147 authored by gabrielhdt's avatar gabrielhdt
Browse files

readme

parent 718811d8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 6 additions and 6 deletions
README.md
+ 6
− 6
View file @ 5ddd2147
# PVS proofs
Encodings of PVS and manual translations of PVS prelude. Use with `lambdapi`.
Encodings of PVS and manual translations of PVS prelude and others.
Use with `lambdapi`.
## TODO
- simplify PVS cert encoding:
- no `Rule` since PTS is functional,
- no `Type Prop Type` rule since it does not concern products but only
predicate subtyping.
## Structure
- `prelude` contains parts of the PVS prelude
- `adlib` contains additional libraries not in the prelude
- `sandbox` contains miscellaneous experiments
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment