From 30f7c63ce566c993816607f3368c357233693aae Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 27 Aug 2024 01:44:45 +0200 Subject: Experimental working commit, programm will compile But the Proof that the domain of the local function is not right. Also if in the definition of our local function we just use f(x) = x then we get a technical ambigus parse --- source/Syntax/Adapt.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'source/Syntax/Adapt.hs') diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 3cff497..4b43bc6 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -34,8 +34,8 @@ scanChunk ltoks = matchOrErr struct "struct definition" pos Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> matchOrErr inductive "inductive definition" pos - Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> - matchOrErr signatureIntro "signature" pos + --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> + -- matchOrErr signatureIntro "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon -- cgit v1.2.3