hipspec
A hip inductive theorem prover!
파일 탐색기
최종 버전 다운로드 (.zip)- Arrays.hs
- DifficultRotate.hs
- Exp.hs
- integers
- Integers.hs
- README.md
- SameFringe.hs
- SnocRotate.hs
- Bool.hs
- Description.org
- Expr.hs
- Fix.hs
- Functions.hs
- Infinite.hs
- InsertionSort.hs
- Integers.hs
- IWC.hs
- MergeSort.hs
- MonadEnv.hs
- MonadMaybe.hs
- MonadState.hs
- Nat.hs
- Nat2ndArg.hs
- NatAcc.hs
- NatDouble.hs
- NatDoubleSlow.hs
- NatStrict.hs
- NatSwap.hs
- Ordinals.hs
- PatternMatching.hs
- ProductiveUseOfFailure.hs
- Queues.hs
- Reverse.hs
- Sequences.hs
- Streams.hs
- Tricky.hs
- ZenoLists.hs
- Count.hs
- ListMonad.hs
- Nat.hs
- Reverse.hs
- Rotate.hs
- BinLists.hs
- BinLists2.hs
- Bool.hs
- Count.hs
- Implications.hs
- InsertionSort.hs
- ListFunctions.hs
- ListMonad.hs
- Lists.hs
- Lists2.hs
- Lists3.hs
- MapCompose.hs
- NaivePQ.hs
- Nat.hs
- Nat2.hs
- Patricia.hs
- ProductiveUseOfFailure.hs
- ProductiveUseOfFailure2.hs
- Queue.hs
- Reverse.hs
- ReverseAsFoldl.hs
- SetList.hs
- ZenoLists.hs
- AppendLists.hs
- BoolExp.hs
- Iterate.hs
- ListMonad.hs
- MapIter.hs
- MergeSort.hs
- QuickSort.hs
- README.md
- Tree2.hs
- Sanity.hs
- TypeSig.hs
- BExp.hs
- BinLists.hs
- CFG.hs
- CFG2.hs
- CFG3.hs
- CFG4.hs
- CFG5.hs
- CFG6.hs
- Concat.hs
- Flatten.hs
- Flatten3.hs
- HOF.hs
- List.hs
- Nat.hs
- Nichomachus.hs
- Ordinals.hs
- PQ.hs
- Properties.hs
- Reverse.hs
- Rotate.hs
- Russel.hs
- SnocReverse.hs
- Sorting.hs
- Invoke.hs
- Provers.hs
- Results.hs
- Calls.hs
- FreeTyCons.hs
- Unfoldings.hs
- Utils.hs
- Associativity.hs
- CallGraph.hs
- Types.hs
- CoreLint.hs
- CoreToRich.hs
- DataConPattern.hs
- Deappify.hs
- FunctionalFO.hs
- LintRich.hs
- Monomorphise.hs
- PolyFOL.hs
- PrettyAltErgo.hs
- PrettyFO.hs
- PrettyRich.hs
- PrettySMT.hs
- PrettyTFF.hs
- PrettyUtils.hs
- RemoveDefault.hs
- Renamer.hs
- Rich.hs
- RichToSimple.hs
- Scope.hs
- Simple.hs
- SimpleToFO.hs
- SimplifyRich.hs
- ToPolyFOL.hs
- TyAppBeta.hs
- Type.hs
- TypedScope.hs
- Uniquify.hs
- Repr.hs
- Definitions.hs
- Get.hs
- Make.hs
- QSTerm.hs
- Resolve.hs
- Scope.hs
- Symbols.hs
- Colour.hs
- PopMap.hs
- ZEncode.hs
- Id.hs
- Induction.hs
- Init.hs
- Lemma.hs
- Lint.hs
- Literal.hs
- Main.hs
- MainLoop.hs
- MakeInvocations.hs
- MakeProofs.hs
- Messages.hs
- Monad.hs
- Params.hs
- ParseDSL.hs
- Pretty.hs
- Property.hs
- Read.hs
- Reasoning.hs
- Theory.hs
- ThmLib.hs
- Translate.hs
- Trim.hs
- Unify.hs
- Utils.hs
- HipSpec.hs
- abbrev.sty
- callgraph.tex
- code.sty
- eqclasses.tex
- hipspec-picture.tex
- mathpartir.sty
- presentation.pdf
- presentation.tex
- prooftree.sty
- QRev.hs
- terms.tex
- .gitignore
- Makefile
- Nicomachus.hs
- result.json
- Reverse.hs
- Rotate.hs
- app.js
- Makefile
- .gitignore
- app.coffee
- index.css
- index.html
- index.sass
- Serve.hs
- .gitignore
- Makefile
- PrecisionRecall.hs
- result.json
- Definitions.skeleton
- mk_zeno_files.py
- PropT01.hs
- PropT02.hs
- PropT03.hs
- PropT04.hs
- PropT05.hs
- PropT06.hs
- PropT07.hs
- PropT08.hs
- PropT09.hs
- PropT10.hs
- PropT11.hs
- PropT12.hs
- PropT13.hs
- PropT14.hs
- PropT15.hs
- PropT16.hs
- PropT17.hs
- PropT18.hs
- PropT19.hs
- PropT20.hs
- PropT21.hs
- PropT22.hs
- PropT23.hs
- PropT24.hs
- PropT25.hs
- PropT26.hs
- PropT27.hs
- PropT28.hs
- PropT29.hs
- PropT30.hs
- PropT31.hs
- PropT32.hs
- PropT33.hs
- PropT34.hs
- PropT35.hs
- PropT36.hs
- PropT37.hs
- PropT38.hs
- PropT39.hs
- PropT40.hs
- PropT41.hs
- PropT42.hs
- PropT43.hs
- PropT44.hs
- PropT45.hs
- PropT46.hs
- PropT47.hs
- PropT48.hs
- PropT49.hs
- PropT50.hs
- Zeno.hs
- zeno_json_wrapper.py
- ZenoVersion.hs
- .gitignore
- Definitions.hs
- Makefile
- Properties.hs
- result.json
- Sorting.hs
- zeno_results.json
- .gitignore
- Definitions.hs
- Makefile
- Properties.hs
- result.json
- Makefile.common
- DataList.hs
- Integer.hs
- DepthTwoCase.hs
- Int.hs
- Let.hs
- PolyLet.hs
- Rank2.hs
- Risers.hs
- App.hs
- BExp.hs
- BinLists.hs
- CAFCase.hs
- ConstLetLambda.hs
- Defaults.hs
- Eithers.hs
- Filter.hs
- Fix.hs
- Guards.hs
- Inner.hs
- IWC.hs
- Lambdas.hs
- LiftTest.hs
- ListsAndLambdas.hs
- Map.hs
- Merge.hs
- MiniApp.hs
- Mutual.hs
- Ordinals.hs
- Partition.hs
- Patterns.hs
- Ptr.hs
- PuoF.hs
- RetPtr.hs
- run_tests.sh
- Sections.hs
- Shadowing.hs
- SimpleLet.hs
- SK.hs
- SomePrelude.hs
- State.hs
- Subtraction.hs
- TypeSynonym.hs
- UnreachableCase.hs
- Vardep.hs
- Where.hs
- Xor.hs
- cabal-apt-install
- .gitignore
- .travis.yml
- hipspec.cabal
- LICENSE
- README.md
- run_tests.sh
- Setup.hs
- stack.yaml
# 설치 가이드
1. 코드 내려받기
git clone https://github.com/danr/hipspec
깃허브에서 프로젝트 코드 전체를 내 컴퓨터로 내려받습니다.
cd hipspec
방금 내려받은 프로젝트 폴더 안으로 이동합니다.
2. Make
보통 추천사전 준비물
- Git GitHub에서 프로젝트 코드를 내려받으려면 필요합니다.
- Make Linux/macOS는 보통 기본 설치되어 있습니다. Windows는 별도 설치(예: MSYS2, WSL)가 필요합니다.
⚠️ 이 프로젝트는 규모가 큰 저장소라, 이 방법이 실제 핵심 제품이 아니라 내부 하위 패키지를 가리키는 것일 수 있습니다. README 전체를 함께 확인해보세요.
cd testsuite/frontend/lib
이 프로젝트의 관련 파일이 하위 폴더 안에 있어서, 먼저 그 폴더로 이동합니다.
make
생성된 빌드 설정을 바탕으로 실제 컴파일을 진행해 실행 파일을 만듭니다.
에러 없이 끝나면 성공입니다. 생성된 실행 파일을 직접 실행해보세요.
// repository documentation
Was this content helpful?
(0 ratings)