wball/fol_idris
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

auto implicits!

Browse source
This commit is contained in:
William Ball 2025-08-13 22:40:17 -07:00
parent 09a7875f03
commit 7eb7a810d6
No known key found for this signature in database
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Proof.idr
View file

@ -22,4 +22,4 @@ data Proof : Context sig g -> Formula sig n -> Type where
ImpE : Proof c (Imp phi psi) -> Proof c phi -> Proof c psi ImpE : Proof c (Imp phi psi) -> Proof c phi -> Proof c psi
ForallI : Proof c phi -> Proof c (Forall phi) ForallI : Proof c phi -> Proof c (Forall phi)
ForallE : Proof c (Forall phi) -> Proof c (elimBinder t phi) ForallE : Proof c (Forall phi) -> Proof c (elimBinder t phi)
Weaken : Proof c1 phi -> Subset c1 c2 -> Proof c2 phi Weaken : Proof c1 phi -> Subset c1 c2 => Proof c2 phi

6
src/Test.idr
View file

@ -113,7 +113,7 @@ doubleNeg :
Proof c (Not (Not phi)) -> Proof c phi Proof c (Not (Not phi)) -> Proof c phi
doubleNeg pf = doubleNeg pf =
Contra $ Contra $
ImpE (Weaken pf (Missing Same)) $ ImpE (Weaken pf) $
Hyp 0 Hyp 0
AndI : {d : _} -> {c : _} -> AndI : {d : _} -> {c : _} ->
@ -124,5 +124,5 @@ AndI pfPhi pfPsi =
ImpI $ ImpI $
ImpE ImpE
(ImpE (Hyp 0) $ (ImpE (Hyp 0) $
Weaken pfPhi $ Missing Same) Weaken pfPhi)
(Weaken pfPsi $ Missing Same) (Weaken pfPsi)