oysteikt/sf1
0
0
Fork 0
forked from oysteikt/sf1-template
Code Pull Requests Activity
11 Commits 1 Branch 0 Tags
main
T
Clone
Open with VS Code Open with VSCodium Open with Intellij IDEA
Download ZIP Download TAR.GZ Download BUNDLE
oysteikt 502acf8596 Update README with progress
2026-07-14 15:13:19 +09:00
.devcontainer
Initial commit
2026-03-10 14:42:27 +09:00
_CoqProject
Initial commit
2026-03-10 14:42:27 +09:00
.envrc
Replace shell.nix with flake.nix
2026-07-07 10:59:19 +09:00
.gitignore
Initial commit
2026-03-10 14:42:27 +09:00
AltAuto.v
Initial commit
2026-03-10 14:42:27 +09:00
AltAutoTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Auto.v
Initial commit
2026-03-10 14:42:27 +09:00
AutoTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Basics.v
Complete Basics.v
2026-03-11 16:36:57 +09:00
BasicsTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Bib.v
Initial commit
2026-03-10 14:42:27 +09:00
BibTest.v
Initial commit
2026-03-10 14:42:27 +09:00
deps.svg
Initial commit
2026-03-10 14:42:27 +09:00
Extraction.v
Initial commit
2026-03-10 14:42:27 +09:00
ExtractionTest.v
Initial commit
2026-03-10 14:42:27 +09:00
flake.lock
Replace shell.nix with flake.nix
2026-07-07 10:59:19 +09:00
flake.nix
Replace shell.nix with flake.nix
2026-07-07 10:59:19 +09:00
Imp.v
Initial commit
2026-03-10 14:42:27 +09:00
ImpCEvalFun.v
Initial commit
2026-03-10 14:42:27 +09:00
ImpCEvalFunTest.v
Initial commit
2026-03-10 14:42:27 +09:00
impdriver.ml
Initial commit
2026-03-10 14:42:27 +09:00
ImpParser.v
Initial commit
2026-03-10 14:42:27 +09:00
ImpParserTest.v
Initial commit
2026-03-10 14:42:27 +09:00
ImpTest.v
Initial commit
2026-03-10 14:42:27 +09:00
IndPrinciples.v
Initial commit
2026-03-10 14:42:27 +09:00
IndPrinciplesTest.v
Initial commit
2026-03-10 14:42:27 +09:00
IndProp.v
Initial commit
2026-03-10 14:42:27 +09:00
IndPropTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Induction.v
Complete Induction.v
2026-07-07 15:50:17 +09:00
InductionTest.v
Initial commit
2026-03-10 14:42:27 +09:00
LICENSE
Initial commit
2026-03-10 14:42:27 +09:00
Lists.v
Complete Lists.v
2026-07-07 10:59:31 +09:00
ListsTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Logic.v
Complete Logic.v
2026-07-14 13:10:31 +09:00
LogicTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Makefile
Initial commit
2026-03-10 14:42:27 +09:00
Maps.v
Initial commit
2026-03-10 14:42:27 +09:00
MapsTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Poly.v
Complete Poly.v
2026-07-07 14:51:49 +09:00
PolyTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Postscript.v
Initial commit
2026-03-10 14:42:27 +09:00
PostscriptTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Preface.v
Initial commit
2026-03-10 14:42:27 +09:00
PrefaceTest.v
Initial commit
2026-03-10 14:42:27 +09:00
ProofObjects.v
Complete ProofObjects.v
2026-07-14 15:07:12 +09:00
ProofObjectsTest.v
Initial commit
2026-03-10 14:42:27 +09:00
README.md
Update README with progress
2026-07-14 15:13:19 +09:00
Rel.v
Initial commit
2026-03-10 14:42:27 +09:00
RelTest.v
Initial commit
2026-03-10 14:42:27 +09:00
Tactics.v
Complete Tactics.v
2026-07-08 04:28:06 +09:00
TacticsTest.v
Initial commit
2026-03-10 14:42:27 +09:00

README.md

Software Foundations 1

This is my instance of Software Foundations 1

Progress

  • Basics
  • Induction
  • Lists
  • Poly
  • Tactics
  • Logic
  • IndProp
    • Rel
    • ProofObjects
      • IndPrinciples
    • Maps
      • Imp
        • ImpParser
          • Extraction
        • ImpCEvalFun
        • Auto

Suggested Roadmap

Deps

View Git Blame Copy Permalink
S
Description
coqnbals
Readme MIT 5.5 MiB
Languages
Rocq Prover 99%
Verilog 0.5%
Dockerfile 0.2%
OCaml 0.1%