Skip to content

WIP Smallstep + Types + STLC + StlcProp #50

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 31 commits into
base: develop
Choose a base branch
from
Open

WIP Smallstep + Types + STLC + StlcProp #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
c903c1d
Started to port Smallstep.
jutaro Sep 5, 2018
dd2630f
normalizing_step.
jutaro Sep 5, 2018
dda41dd
Nothing really
jutaro Sep 7, 2018
3d81a1b
eval__multistep
jutaro Sep 13, 2018
5739aaa
Started with text and exercises.
jutaro Sep 19, 2018
21524b6
Adding Exercises.
jutaro Sep 19, 2018
14a5458
Exercises
jutaro Sep 20, 2018
f145647
Fixes
jutaro Sep 20, 2018
b03b894
Add Types.lidr.
jutaro Sep 22, 2018
cf20302
Types up to progress.
jutaro Sep 23, 2018
f0b3f35
Added part of progress proof.
jutaro Sep 24, 2018
f4ba079
Type progress and preservation
jutaro Sep 25, 2018
4227114
Soundness proof.
jutaro Sep 25, 2018
409ff78
Types exercises and formatting.
jutaro Sep 26, 2018
ff80c26
Use operator instead of syntax for iff.
jutaro Sep 26, 2018
2d44378
Add STLC.lidr.
jutaro Sep 26, 2018
86bb04a
Changed syntax for Has_type.
jutaro Sep 26, 2018
430277d
Started Stlc.
jutaro Sep 26, 2018
64fd826
Substitution.
jutaro Sep 29, 2018
b9749fb
Started Reduction.
jutaro Sep 30, 2018
52b5187
Typing of Stlc.
jutaro Oct 1, 2018
b92be28
Finished with Stlc.
jutaro Oct 2, 2018
9615a1b
Started StlcProp
jutaro Oct 18, 2018
feae903
Use Id instead of String.
jutaro Oct 19, 2018
527982b
Substitution
jutaro Oct 19, 2018
290367f
WIP review
Nov 7, 2018
764f83b
Merge branch 'smallstep' of https://github.com/jutaro/software-founda…
Nov 7, 2018
5043995
rewrap text, WIP concurrent Imp
Nov 8, 2018
0b0214d
add small-step Imp & concurrent Imp
Nov 27, 2018
43f0f5b
finish smallstep
Nov 28, 2018
6464d89
Preservation proof
jutaro Jan 10, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions software_foundations.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ modules = Basics
, Rel
, Imp
, ImpParser
, Smallstep

brief = "Software Foundations in Idris"
version = 0.0.1.0
Expand Down
8 changes: 8 additions & 0 deletions src/Maps.lidr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,14 @@ equality comparison function for \idr{Id} and its fundamental property.
> beq_id (MkId n1) (MkId n2) = decAsBool $ decEq n1 n2
>

> idInjective : {x,y : String} -> (MkId x = MkId y) -> x = y
> idInjective Refl = Refl

> implementation DecEq Id where
> decEq (MkId s1) (MkId s2) with (decEq s1 s2)
> | Yes prf = Yes (cong prf)
> | No contra = No (\h : MkId s1 = MkId s2 => contra (idInjective h))

\todo[inline]{Edit}

(The function \idr{decEq} comes from Idris's string library. If you check its
Expand Down
Loading